blob: d8138e145cfde4a03303d938ff3abee529d7e59d (
plain)
1
2
3
4
5
6
7
8
|
Lemma toto (E : nat -> nat -> Prop) (x y : nat)
(Ex_ : forall z, E x z) (E_y : forall z, E z y) : True.
(* OK *)
assert (pairE1 := let Exy := _ in (Ex_ y, E_y _) : Exy * Exy).
(* FAIL *)
assert (pairE2 := let Exy := _ in (Ex_ _, E_y x) : Exy * Exy).
|
