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