How do I move a let variable to a separate hypothesis?

Question

In Coq, as a simplified example (using False to ignore the conclusion),

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (cmplx :=
      let a := f 0 in
      let b := f 1 in
      g a b
    )
    : False.

I want to take the let variables a and b out of the scope of cmplx and make them into separate hypotheses, like

Theorem example
    (f : nat -> bool)
    (g : bool -> bool -> bool)
    (a := f 0)
    (b := f 1)
    (cmplx := g a b)
    : False.

This is easy to prove in specific cases, e.g. with using change directly, or if you can pattern the expressions to catch how the let variables are used,

Theorem let_up {B C D} (b : B) (c : B -> C) (d : C -> D)
    : let r := let a := b in c a in d r = let a := b in let r := c a in d r.
Proof.
  apply eq_refl.
Qed.

Theorem example : ...
Proof.
  revert cmplx.
  (* manually patterning *)
  change (let cmplx := let a := f 0 in (fun a => let b := f 1 in g a b) a in (fun _ => False) cmplx).
  rewrite let_up.
  intros.

Though, this raises a and could be done similarly for b.

Is there a tactic to do this generally? Or, a larger Ltac I could write to handle it automatically? I have a more complex function with many lets that I want to act on separately, so I want to split them out in this way. I can just change it, but it's long enough that that would be annoying. I also tried things like

lazymatch goal with
| H := let _ := ?b in _ |- _ => idtac H "has" b
end.

but, it doesn't seem to let you match the in clause, probably due to non-free variables.

That is, I want to be able to say something like

let_up cmplx a

to raise a out of cmplx.

Edit 1: g is a more complex function, so simpl and similar would make it very large and unreadable. I only want to remove the top let and not make other changes.

Answer 1

set (a:=f 0). 
set (b:=f 1). 
fold a b in cmplx.
simpl in cmplx.

set defines new variables in the context.

fold replaces a term with a definition that is definitionally equal.

simpl can help to "get rid of" let bindings.

EDIT. Ah, now I see you want a tactic that does this automatically.