fact: Record Admissible (P : term -> Prop) := { Admissible_head_exp M N : head_exp P M N -> P M -> P N; Admissible_neutral M : neutral P M -> P M; Admissible_app_var M x : P (app M (var x)) -> P M }.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts List ssreflect