Skip to content

Instantly share code, notes, and snippets.

@qnighy

qnighy/right-associative-intro-pattern.v

Created July 3, 2014 03:07
Show Gist options
  • Save qnighy/41f75649a5d0d8ce31f8 to your computer and use it in GitHub Desktop.
Save qnighy/41f75649a5d0d8ce31f8 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
right-associative-intro-pattern.v
Lemma foo : forall P Q R S : Prop, P /\ Q /\ R /\ S -> S.
Proof.
intros P Q R S (H0 & H1 & H2 & H3); apply H3.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment