Ssreflect Users Discussion List

[Keiko Nakata <>]

Follow-up:

I noticed that the problem only appears with Guarded, but I can Qed
the proof without problems; so the reason is probably Guarded examines
unreduced terms, whereas Qed examines reduced terms. 

Best,
Keiko   

From: <>
Subject: selectors and coinduction
Date: Wed, 18 Feb 2009 16:45:35 +0100 (CET)

> Hello.
> 
> Could first and last tactical unfortunately interact with proof by 
> coinduction?
> 
> I have been correcting my proof to get rid of unguarded recursive calls
> and suspect  a tactic;
> have [h | h] := "something..."; last first 
> of making the unguarded call. 
> 
> kind regards,
> Keiko