blob: 611464458e9a163473044975d2e90f3e25cbf7ed (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Set Implicit Arguments.
Unset Elimination Schemes.
Inductive JMeq (A:Type) (x:A) : forall B:Type, B -> Prop :=
JMeq_refl : JMeq x x.
Set Elimination Schemes.
Register JMeq as core.JMeq.type.
Axiom JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
P x -> forall y, JMeq x y -> P y.
Register JMeq_ind as core.JMeq.ind.
Lemma JMeq_ind_r : forall (A:Type) (x:A) (P:A -> Prop),
P x -> forall y, JMeq y x -> P y.
Proof. intros. try rewrite H0.
Abort.
|
