| John Major's Equality as proposed by C. Mc Bride |
Set Implicit Arguments.
Inductive JMeq (A:Set) (x:A) : forall B:Set, B -> Prop :=
JMeq_refl : JMeq x x.
Reset JMeq_ind.
Hint Resolve JMeq_refl.
Lemma sym_JMeq : forall (A B:Set) (x:A) (y:B), JMeq x y -> JMeq y x.
destruct 1; trivial.
Qed.
Hint Immediate sym_JMeq.
Lemma trans_JMeq :
forall (A B C:Set) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
destruct 1; trivial.
Qed.
Axiom JMeq_eq : forall (A:Set) (x y:A), JMeq x y -> x = y.
Lemma JMeq_ind : forall (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.
Qed.
Lemma JMeq_rec : forall (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.
Qed.
Lemma JMeq_ind_r :
forall (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 := sym_JMeq H'); trivial.
Qed.
Lemma JMeq_rec_r :
forall (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 := sym_JMeq H'); trivial.
Qed.
JMeq is equivalent to (eq_dep Set [X]X)
|
Require Import Eqdep.
Lemma JMeq_eq_dep :
forall (A B:Set) (x:A) (y:B), JMeq x y -> eq_dep Set (fun X => X) A x B y.
Proof.
destruct 1.
apply eq_dep_intro.
Qed.
Lemma eq_dep_JMeq :
forall (A B:Set) (x:A) (y:B), eq_dep Set (fun X => X) A x B y -> JMeq x y.
Proof.
destruct 1.
apply JMeq_refl.
Qed.