proposition: Lemma solution_right_let : forall {A} {B : A -> Type} (b t : A), (t = b -> B t) -> (let x := b in t = x -> B x).
proof: Proof. intros A B b t H x eq. subst x. destruct eq. apply H. reflexivity. Defined.
imports: Coq.Program.Tactics Equations.Init Equations.CoreTactics Equations.Signature Equations.Prop.Logic Equations.Prop.Classes Equations.Prop.EqDec