Library Coq.Logic.JMeq
John Major's Equality as proposed by Conor McBride
Reference:
McBride Elimination with a Motive, Proceedings of TYPES 2000,
LNCS 2277, pp 197-216, 2002.
Inductive JMeq (
A:Type) (
x:A) :
forall B:Type,
B ->
Prop :=
JMeq_refl :
JMeq x x.
Hint Resolve JMeq_refl.
Lemma sym_JMeq :
forall (
A B:Type) (
x:A) (
y:B),
JMeq x y ->
JMeq y x.
Hint Immediate sym_JMeq.
Lemma trans_JMeq :
forall (
A B C:Type) (
x:A) (
y:B) (
z:C),
JMeq x y ->
JMeq y z ->
JMeq x z.
Axiom JMeq_eq :
forall (
A:Type) (
x y:A),
JMeq x y ->
x =
y.
Lemma JMeq_ind :
forall (
A:Type) (
x y:A) (
P:A ->
Prop),
P x ->
JMeq x y ->
P y.
Lemma JMeq_rec :
forall (
A:Type) (
x y:A) (
P:A ->
Set),
P x ->
JMeq x y ->
P y.
Lemma JMeq_rect :
forall (
A:Type) (
x y:A) (
P:A->Type),
P x ->
JMeq x y ->
P y.
Lemma JMeq_ind_r :
forall (
A:Type) (
x y:A) (
P:A ->
Prop),
P y ->
JMeq x y ->
P x.
Lemma JMeq_rec_r :
forall (
A:Type) (
x y:A) (
P:A ->
Set),
P y ->
JMeq x y ->
P x.
Lemma JMeq_rect_r :
forall (
A:Type) (
x y:A) (
P:A ->
Type),
P y ->
JMeq x y ->
P x.
JMeq is equivalent to eq_dep Type (fun X => X)
eq_dep U P p x q y is strictly finer than JMeq (P p) x (P q) y