proposition: Lemma head_exp'I M N : head_exp sn M N -> exists L, head_exp' sn M N L.
proof: Proof. elim; by firstorder (eauto using head_exp'). Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations List Wellfounded.Transitive_Closure ssreflect