Skip to content

Instantly share code, notes, and snippets.

@autotaker

autotaker/CoqEx19.v

Created May 11, 2014 14:57
Show Gist options
  • Save autotaker/a97f89ffee3e96cfedb6 to your computer and use it in GitHub Desktop.
Save autotaker/a97f89ffee3e96cfedb6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
CoqEx19.v
Parameter A : Set.
Definition Eq (a : A) (b : A) : Prop :=
forall (f : A -> Prop), f a <-> f b.
Lemma Eq_eq : forall x y, Eq x y <-> x = y.
Proof.
intros.
split.
intro.
unfold Eq in H.
specialize (H (fun a => a = y)).
destruct H.
apply H0.
reflexivity.
intro.
unfold Eq.
intros.
subst.
apply iff_refl.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment