proposition: Lemma step_step' M N : step M N -> exists N', step' M N'.
proof: Proof. elim: M N. - by move=> > /stepE. - move=> [?|M1 M2|M] IHM N IHN ?. + move=> /stepE [|[|]] [?] [] => [|/stepE|]; [done..|]. move=> /IHN [?] [] ? _. * eexists. left. apply: stepIAppR. by eassumption. * eexists. right. by apply: stepKNAppR; [constructor|eassumption]. + have [[?]|H] := step_dec (app M1 M2). * move=> /IHM [?] []; by eauto using stepK, stepI. * move=> /stepE [|[|]] [?] [] => [|/H|]; [done..|]. move=> /IHN [?] []; [by eauto using stepK, stepI|]. move=> ? _. eexists. right. apply: stepKNAppR; [|by eassumption]. move: H => /not_step_normal_form /normal_form_app_neutral. by apply: neutral_impl. + have [?|[? ->]] := has_var_zero_dec M. { by eauto using stepK, stepI. } have [[?]|/not_step_normal_form ?] := step_dec N. * move=> /IHN [?] []; by eauto using stepK, stepI. * by eauto using stepK, stepI. - move=> ? IH ? /stepE [?] [/IH [? [?|?]]]. + by eauto using stepK, stepI. + by eauto using stepK, stepI. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect