proposition: Lemma head_expE (P : term -> Prop) M N : head_exp P M N -> match N with | var _ => False | app N1 N2 => (exists N1', N1 = lam N1' /\ M = (subst (scons N2 var) N1') /\ P N2) \/ (exists M1, M = app M1 N2 /\ head_exp P M1 N1 /\ P N2) | lam _ => False end.
proof: Proof. case=> *; [left|right]; by do ? econstructor. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect