proposition: Theorem fundamental (P : term -> Prop) Gamma M t : Admissible P -> type_assignment Gamma M t -> P M.
proof: Proof. move=> /[dup] HP /satisI /[apply] /(_ var). rewrite subst_var_term. have HQ := Admissible_Saturated_interp HP. move=> H. apply: (Saturated_incl (HQ _)). apply: H=> i *. have : neutral P (var i) by constructor. by split; [|apply /Forall_forall]=> *; apply: (Saturated_neutral (HQ _)). Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect