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