fact: Definition Arr (P Q : term -> Prop) (M : term) := forall N, P N -> Q (app M N).
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect