proposition: Lemma sn_step'_nf M : sn M -> exists N, steps' M N /\ normal_form N.
proof: Proof. elim=> {}M _ IH. case: (step'_or_nf M). - move=> [?] /[dup] /step'_step /IH [?] [??] ?. eexists. split; [|by eassumption]. apply: rt_trans; [apply: rt_step|]; by eassumption. - move=> ?. eexists. by split; [apply: rt_refl|]. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect