proposition: Lemma stepLam' s t t' : t' = (subst (scons t var) s) -> step (app (lam s) t) t'.
proof: Proof. move=> ->. by apply: wCBN_stepSubst. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect