Skip to content

Instantly share code, notes, and snippets.

@sunaemon

sunaemon/19.v

Last active August 29, 2015 14:00
Show Gist options
  • Save sunaemon/11349628 to your computer and use it in GitHub Desktop.
Save sunaemon/11349628 to your computer and use it in GitHub Desktop.
Download ZIP
Coq演習
Raw
19.v
Parameter A : Set.
Definition Eq := fun a b:A => forall ee : A->A->Prop, ee a a -> ee a b.
Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros x y.
unfold Eq.
split.
+ intro H.
exact (H eq eq_refl).
+ intro H.
rewrite <- H.
tauto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment