proposition: Lemma interp_head_exp {P : term -> Prop} {M N t} : Admissible P -> head_exp P M N -> interp P M t -> interp P N t.
proof: Proof. move=> HP. have HQ := Admissible_Saturated_interp HP. elim: t M N. { move=> *. apply: (Admissible_head_exp _ HP); eassumption. } move=> s ? phi t IH M N /= ? IH' N' [Hs Hphi]. apply: IH. { constructor; [|apply: (Saturated_incl (HQ _))]; eassumption. } by apply: IH'. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect