proposition: Lemma weak_normalization {Gamma M t} : type_assignment Gamma M t -> wn M.
proof: Proof. apply: fundamental. by apply: Admissible_wn.Admissible_wn. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect