fact: Record Saturated (Q P : term -> Prop) := { Saturated_incl : forall M, P M -> Q M; Saturated_neutral : forall M, neutral Q M -> P M }.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect