coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Benedikt AHRENS <Benedikt.Ahrens AT unice.fr>
- To: "Edward Z. Yang" <ezyang AT mit.edu>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Induction/destruct over a type with extra structure, redux
- Date: Thu, 03 Nov 2011 17:51:35 +0100
Hello,
On 11/03/2011 05:14 PM, Edward Z. Yang wrote:
Lemma cop'_op : forall se se', cop' se se' -> op se se'.
induction 1. destruct H.
Abort.
try "inversion H." instead of "destruct H.".
This will give you the useful info you need to finish the proof.
benedikt
- [Coq-Club] Induction/destruct over a type with extra structure, redux, Edward Z. Yang
- Re: [Coq-Club] Induction/destruct over a type with extra structure, redux, Benedikt AHRENS
Archive powered by MhonArc 2.6.16.