proposition: Lemma contains_many_poly_absE {n s1 t1 t} : contains (many_poly_abs n (poly_arr s1 t1)) t -> exists ts, length ts <= n /\ t = subst_poly_type (fold_right scons poly_var ts) (many_poly_abs (n - length ts) (poly_arr s1 t1)).
proof: Proof. move=> /clos_rt_rtn1_iff. elim. - exists [] => /=. constructor; first by lia. by rewrite (ltac:(lia) : n - 0 = n) subst_poly_type_poly_var. - move=> > [] r ? _ [ts] [?]. move Hn': (n - length ts) => n'. case: n' Hn'; first done. move=> n' ? [->]. exists (r :: ts) => /=. constructor; first by lia. have ->: n - S (length ts) = n' by lia. rewrite ?poly_type_norm. apply: ext_poly_type. case; first done. move=> x /=. by rewrite ?poly_type_norm /= subst_poly_type_poly_var. 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