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