proposition: Lemma wn_ren xi M : wn (ren xi M) -> wn M.
proof: Proof. case=> N /steps_renE [?] [->] ? /normal_form_ren' /wn_intro. by apply. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect