fact: Definition many_argument_app (P: term) (As: list argument) := fold_left (fun P A => match A with | argument_term Q => app P Q | argument_poly_type t => ty_app P t end) As P.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts) ssreflect ssrbool ssrfun