proposition: Lemma step'_step_det M N : step' M N -> forall N', step M N' -> N = N'.
proof: Proof. elim. - move=> {}M {}N HM HN N'. move E: (app (lam M) N) => M' H. case: H E. + congruence. + move=> > /normal_form_not_step H [] ??. subst. case: H. by constructor. + move=> > /normal_form_not_step H [] ??. by subst. + done. - move=> M1 M2 {}N HN HM1M2 HM1 N'. move E: (app M1 N) => M' H. case: H E. + move=> > [] ??. subst. by move=> /step'E in HM1M2. + move=> > H [] ??. subst. congr app. by apply: HM1. + move=> > /normal_form_not_step ? [] ??. by subst. + done. Qed.
imports: Undecidability.LambdaCalculus(Krivine Lambda Util.Krivine_facts) Undecidability.LambdaCalculus.Util.term_facts Undecidability.Shared.deterministic_simulation Relations List ssreflect