proposition: Lemma Admissible_Saturated_interp {P} : Admissible P -> forall t, Saturated P (fun M => interp P M t).
proof: Proof. move=> HP. elim /sty_ind'. { move=> x. constructor=> ?. - done. - by apply: (Admissible_neutral P HP). } move=> s phi t IHs IHphi IHt. constructor=> M /= HM. - have /HM : interp P (var 0) s /\ all (interp P (var 0)) phi. { split. - apply: (Saturated_neutral IHs). by constructor. - apply /Forall_all. apply: Forall_impl IHphi=> ?. move=> /Saturated_neutral. apply. by constructor. } move=> /(Saturated_incl IHt). by apply: (Admissible_app_var P HP). - move=> N [+ _] => /(Saturated_incl IHs) ?. apply: (Saturated_neutral IHt). by constructor. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect