Skip to content

Instantly share code, notes, and snippets.

@KeenS

KeenS/1-5.v

Created April 7, 2014 15:25
Show Gist options
  • Save KeenS/10022411 to your computer and use it in GitHub Desktop.
Save KeenS/10022411 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
1-5.v
Lemma NotNot : forall P : Prop, P -> ~~P.
Proof.
intros.
unfold not.
intros.
apply H0.
apply H.
Qed.
Require Import Classical.
Theorem NotNot_LEM : forall P : Prop, ~~(P \/ ~P).
Proof.
intro P.
apply NotNot.
apply classic.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment