proposition: Lemma step'_step M N : step' M N -> step M N.
proof: Proof. elim=> *. - by apply: stepSubst. - by apply: stepAppL. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect