The Coq mailing list

[Jean-Marc Notin <notin AT lix.polytechnique.fr>]

> It seems the induction tactic didn't generate the hypotheses (s =
> (a1,b1)) and (s = (a2,b2)). What's happening here, and how can I fix
> it? I'm using Coq 8.1gamma.
> 
In such a case, you can try to use the 'inversion' tactic, or, if it is
not powerful enough, you can do something like this:

intros a1 b1 a2 b2; set (c1 := (a1,b1)); set  (c2 := (a2,b2)); assert
(c1=(a1,b1)) by trivial; assert (c2=(a2,b2)) by trivial; clearbody c1;
clearbody c2. 
induction 1.

-- 
Jean-Marc Notin 
<notin AT lix.polytechnique.fr>
LIX

Attachment: signature.asc
Description: Ceci est une partie de message numériquement signée