blob: 9c96ae021e51d68814b518f755e83cd17911f70f (
plain)
1
2
3
4
5
6
7
8
9
10
|
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).
Abort.
|
