proposition: Lemma let_binding_unfold : forall (A B:Type) (v:A) (K:A->B), let_binding v K = K v.
proof: Proof. Proof using. reflexivity. Qed.
imports: Coq.Lists.List Coq.Logic.ProofIrrelevance Coq.Program.Equality Coq.Arith.Compare_dec Coq.micromega.Lia