blob: 61882176aa81b19a3379def1a21528d1c4cb47b2 (
plain)
1
2
3
4
5
6
7
8
9
|
(* Check that metas are whd-normalized before trying 2nd-order unification *)
Lemma test :
forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop),
(forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A))
-> Q D (T D).
Proof.
intros D T Q H.
pattern (T D). apply H.
Qed.
|
