1 files changed, 37 insertions, 0 deletions
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
new file mode 100644
index 0000000000..2f8eda34f5
--- /dev/null
+++ b/theories/Logic/JMeq.v
@@ -0,0 +1,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.