Skip to content

Instantly share code, notes, and snippets.

@kencoba

kencoba/NaturalDeduction_p18.v

Created May 10, 2011 01:39
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 kencoba/963772 to your computer and use it in GitHub Desktop.
Save kencoba/963772 to your computer and use it in GitHub Desktop.
Download ZIP
NaturalDeduction Dag Prawitz p18
Raw
NaturalDeduction_p18.v
Section NaturalDeduction_p18.
Variable D : Set.
Variable P : D -> D -> Prop.
Hypothesis Pxy : forall x, exists y, P x y.
Hypothesis PxyPyx : forall x y,(P x y) -> (P y x).
Lemma p18 : forall x, exists y, (P x y) /\ (P y x).
Proof.
intros x.
elim (Pxy x).
intros y Pxy'.
exists y.
split.
apply Pxy'.
apply (PxyPyx x y).
apply Pxy'.
Qed.
End NaturalDeduction_p18.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment