proposition: Lemma satisI P Gamma M t : Admissible P -> type_assignment Gamma M t -> satis P Gamma M t.
proof: Proof. move=> HP. have HQ := Admissible_Saturated_interp HP. elim: M Gamma t. - move=> a > /type_assignmentE [] s phi Ha H. move=> sigma /(_ a _ _ Ha) [] /=. case: H. { by move=> <-. } by move=> + _ /Forall_forall {}H => /H. - move=> ? IH1 ? IH2 ?? /type_assignmentE [] s phi /IH1 /= {}IH1 /IH2 {}IH3 Hphi. move=> sigma Hsigma /=. apply: (IH1 sigma Hsigma). split. { by apply: IH3. } apply /Forall_all. apply: Forall_impl Hphi => ? /IH2. by apply. - move=> ? IH1 ? [?|s phi t] /type_assignmentE; first done. move=> /IH1 {}IH1 sigma HGamma /=. move=> N [Hs Hphi]. apply: (interp_head_exp HP). { apply: head_exp_lam. by apply: (Saturated_incl (HQ s)). } rewrite subst_subst_term. apply: IH1=> - [|i]. + move=> /= ?? [<- <-]. by split; [|apply /Forall_all]. + move=> ?? /HGamma => - [Hs' Hphi'] /=. by rewrite !simpl_term. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect