proposition: Lemma wn_app_var M x : wn (app M (var x)) -> wn M.
proof: Proof. case=> N /clos_rt_rt1n_iff. move E: (app M (var x)) => M' H. elim: H M E. { move=> ?? E H. case: H E; [done|done|..]. - move=> > ? [] -> _. by econstructor; [apply: rt_refl|constructor]. - move=> > ?? [] -> _. by econstructor; [apply: rt_refl|]. } move=> > []. - move=> > IH ?? [??]. subst. move: IH. rewrite subst_as_ren. by move=> /clos_rt_rt1n_iff /wn_intro /[apply] /wn_ren /wn_lam. - move=> > ?? IH ? [??]. subst. move: (IH _ eq_refl) => /[apply]. by apply: step_wn. - move=> > H ? IH ? [??]. subst. by move=> /stepE in H. - done. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect