proposition: Lemma contains_many_poly_abs_free {n x t} : contains (many_poly_abs n (poly_var (n + x))) t -> exists i m, n = i + m /\ t = many_poly_abs m (poly_var (m+x)).
proof: Proof. elim: n x t. - move=> /= x ? /containsE <-. by exists 0, 0. - move=> n IH x t /containsE /= []. + move=> <-. by exists 0, (1+n). + move=> [?]. rewrite subst_poly_type_many_poly_abs /=. have ->: S (n + x) = n + S x by lia. rewrite iter_up_poly_type_poly_type /=. move=> /IH [i] [m] [-> ->]. by exists (1+i), m. Qed.
imports: List Lia Relation_Definitions Relation_Operators Operators_Properties Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts iipc2_facts) ssreflect ssrbool ssrfun