Skip to content

Instantly share code, notes, and snippets.

@maedaunderscore

maedaunderscore/ogic example.v

Created July 18, 2015 07:53
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 maedaunderscore/4731519594f55bb79511 to your computer and use it in GitHub Desktop.
Save maedaunderscore/4731519594f55bb79511 to your computer and use it in GitHub Desktop.
Download ZIP
logic example.v exo0
Raw
ogic example.v
Lemma exo0 : forall P : Prop, P -> P.
Proof.
move=> P.
move=> P2.
apply P2.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment