The Coq mailing list

[Tom Payne <thp AT cs.ucr.edu>]

How do I use instances of multivariable propositional lemmas in a
subsequent proof?

Suppose I've proved a lemma, call it mylemma.  If it involves only one
propositional variable, I can subsequently use instances of it in
tactics, e.g., "case(mylemma(Q->R\/~R))."  But what if mylemma
involves two propositional varaiables, say P and Q ?  How can I
substitute say R\/~R for P and ~R for Q in mylemma and have a tactic
use that instance?  So far, my reading the manual and use of the
empirical method have failed to find an answer.

Tom Payne

P.S.: I'm new to Coq.