Skip to content

Instantly share code, notes, and snippets.

@satos---jp

satos---jp/coq_practice_19.v

Created May 11, 2014 14:10
Show Gist options
  • Save satos---jp/0a9f74599b55615a9914 to your computer and use it in GitHub Desktop.
Save satos---jp/0a9f74599b55615a9914 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
coq_practice_19.v
Parameter A : Set.
Definition Eq : A -> A -> Prop :=
fun p q => p = q.
Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros.
unfold Eq.
apply iff_refl.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment