proposition: Lemma Admissible_wn : Admissible wn.
proof: Proof. constructor. - by apply: head_exp_wn. - by apply: neutal_wn_wn. - by apply: wn_app_var. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect