Hi all,

So, I have an example the following proof context :

a := b+c : nat

H : a <> 0

I wanted to replace the value of a (b+c) in the hypothesis H, tried apply/rewrite tactics but nothing worked.

The value of a is actually a part in my lemma defined with let, so I should be able to manipulate as I want :

Lemma x : …

let a := b+c in

…

Any explanation ?

Thanks

Lili