The Coq mailing list

[Ewen Denney <denney AT irisa.fr>]

Salut,

What is the general way of going about `unfolding lets'? The folowing
example shows the kind of thing:

Variable f : nat -> nat*nat.
Hypothesis H : (n:nat) ((Fst (f n)) = O).

Goal  let (n,_) = (f O) in (n=O).

The example I actually have is where f is some complicated thing defined
elsewhere and I want to move the binding n = Fst (f O) up into the
assumptions somehow, so that I can work on the body.


Ewen