Skip to content

Instantly share code, notes, and snippets.

@qnighy

qnighy/eqdep_jmeq.v

Created April 18, 2014 13:04
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save qnighy/11043236 to your computer and use it in GitHub Desktop.
Save qnighy/11043236 to your computer and use it in GitHub Desktop.
Download ZIP
Eqdep implies JMeq_eq
Raw
eqdep_jmeq.v
Require Import Eqdep.
Set Implicit Arguments.
Inductive JMeq (A : Type) (x : A) : forall B : Type, B -> Prop :=
JMeq_refl : JMeq x x.
Lemma JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
Proof.
intros A x y H.
apply (inj_pair2 Type (fun t => t)).
destruct H.
reflexivity.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment