Rewrite variable value in hypothesis

Using Coq
1

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

2

subst a does the trick here.

1 Like