proposition: Lemma neutal_wn_wn M : neutral wn M -> wn M.
proof: Proof. suff: neutral wn M -> exists N, clos_refl_trans term step M N /\ neutral normal_form N. { move=> /[apply] - [N] [??]. exists N; [done|by apply: neutral_normal_form]. } elim. { move=> x. exists (var x). by split; [apply: rt_refl|constructor]. } move=> {}M N H1M [M'] [HMM' HM'] [N'] HNN' HN'. exists (app M' N'). split; [|by constructor]. apply: (rt_trans _ _ _ (app M' N)). - by apply: rt_stepsAppL. - by apply: rt_stepsAppR. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect