The Coq mailing list

[Math Prover <mathprover AT gmail.com>]

Hi,

  I want to destruct a "scoped and". See attached tac.v

  My existing implementation is somewhat ugly -- for each length, I need to create (a) two lemmas and (b) an extra line in the tactic.

  I was wondering if there was a simpler way to do this in "one shot"

Attachment: tac.v
Description: Binary data