proposition: Lemma cbv_step_to_lam s1 s2 t : cbv_step (app s1 s2) (lam t) -> exists s1' s2', s1 = lam s1' /\ s2 = lam s2' /\ lam t = subst (scons (lam s2') var) s1'.
proof: Proof. move Es': (app s1 s2) => s'. move Et': (lam t) => t' Hs't'. elim: Hs't' s1 s2 t Es' Et'; [|done|done]. move=> > [? ?] ?. do 2 eexists. by split; [eassumption|split; [eassumption|]]. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)