blob: 2f8eda34f55a9fee5f9ef9e4ce07d9f3149f68bd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(*s John Major's Equality - C. Mc Bride *)
Set Implicit Arguments.
Inductive JMeq [A:Set;x:A] : (B:Set)B->Prop :=
JMeq_refl : (JMeq x x).
Hints Resolve JMeq_refl.
Lemma JMeq_sym : (A,B:Set)(x:A)(y:B)(JMeq x y)->(JMeq y x).
Destruct 1; Trivial.
Save.
Hints Immediate JMeq_sym.
Lemma JMeq_trans : (A,B,C:Set)(x:A)(y:B)(z:C)
(JMeq x y)->(JMeq y z)->(JMeq x z).
Destruct 1; Trivial.
Save.
Axiom JMeq_eq : (A:Set)(x,y:A)(JMeq x y)->(x=y).
Lemma JMeq_eq_ind : (A:Set)(x,y:A)(P:A->Prop)(P x)->(JMeq x y)->(P y).
Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
Save.
Lemma JMeq_eq_rec : (A:Set)(x,y:A)(P:A->Set)(P x)->(JMeq x y)->(P y).
Intros A x y P H H'; Case JMeq_eq with 1:=H'; Trivial.
Save.
Lemma JMeq_eq_ind_r : (A:Set)(x,y:A)(P:A->Prop)(P y)->(JMeq x y)->(P x).
Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
Save.
Lemma JMeq_eq_rec_r : (A:Set)(x,y:A)(P:A->Set)(P y)->(JMeq x y)->(P x).
Intros A x y P H H'; Case JMeq_eq with 1:=(JMeq_sym H'); Trivial.
Save.
|
