blob: 5f5421ac74a6950895ff31e4fcbe8aa84f0b5708 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Require Import ssreflect ssrbool.
Axiom eqn : nat -> nat -> bool.
Infix "==" := eqn (at level 40).
Axiom eqP : forall x y : nat, reflect (x = y) (x == y).
Lemma test1 :
forall x y : nat, x = y -> forall z : nat, y == z -> x = z.
Proof.
by move=> x y + z /eqP <-; apply.
Qed.
Lemma test2 : forall (x y : nat) (e : x = y), e = e -> x = y.
Proof.
move=> + y + _ => x def_x; exact: (def_x : x = y).
Qed.
Lemma test3 :
forall x y : nat, x = y -> forall z : nat, y == z -> x = z.
Proof.
move=> ++++ /eqP <- => x y e z; exact: e.
Qed.
|
