proposition: Lemma step'_det M N N' : step' M N -> step' M N' -> N = N'.
proof: Proof. move=> /step'_step_det H /step'_step. by apply: H. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect