Improve apply

In some cases, we would like apply to perform matching on hypothesis too. Coq can do that in:

Goal forall P Q, (forall x y, P x y -> Q) -> P 3 4 -> Q.
intros P Q H H1.
apply H with (1:=H1).

We could imagine:

apply H with_hyp H1

To be investigated.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information