Hi all,

Is there a simple tactic to deal with a let binding in a hypothesis in a nice way? In particular, do this:

```
Lemma foo : forall k, let kk := k + k in 2 * k = kk. (* example with let *)
Proof.
(* note that intros / simpl and let work nicely together *)
intros k kk. simpl. now rewrite <- plus_n_O.
Qed.
Goal False.
Proof.
pose proof (H := foo 42). (* we use the example with let *)
(* find a nicer way to do this next line *)
pose (kk := 42 + 42). change (2 * 42 = kk) in H.
```

but with manual `pose`

and `change`

? (my actual use case is a large formula)

`destruct`

does not work since destructs the underlying equality, seeing right through the `let`

:sad:

`set (kk := 42 + 42) in H. cbv zeta in H.`

? maybe a `match goal`

can let you avoid having to write 42+42

that kind of works, thanks. but it breaks if there's two let-binds

Is there a way in Ltac(2) to substitute the topmost bound variable of a gallina term?

Last updated: Jun 22 2024 at 15:01 UTC