proposition: Lemma head_exp_wn M N : head_exp wn M N -> wn M -> wn N.
proof: Proof. by move=> /head_exp_step /step_wn. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect