proposition: Lemma head_exp_step M N : head_exp wn M N -> step N M.
proof: Proof. elim. { move=> *. by apply: stepSubst. } move=> *. by apply: stepAppL. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect