proposition: Lemma wn_lam M : wn M -> wn (lam M).
proof: Proof. case=> N HMN ?. apply: (wn_intro (lam N)); [|by constructor]. elim: HMN; by eauto using clos_refl_trans, step with nocore. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect