Skip to content

Instantly share code, notes, and snippets.

@pasberth

pasberth/mp.v

Created December 31, 2013 05:27
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save pasberth/8192961 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save pasberth/8192961 to your computer and use it in GitHub Desktop.
Download ZIP
Modus ponens
Raw
mp.v
Theorem Modus_ponens: forall (P Q: Prop), (P -> Q) -> P -> Q.
Proof.
intro P.
intro Q.
intro H.
apply H.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment