proposition: Lemma contains_subst_poly_type_fold_rightI {ts t} : contains (many_poly_abs (length ts) t) (subst_poly_type (fold_right scons poly_var ts) t).
proof: Proof. elim: ts t. - move=> /= ?. rewrite subst_poly_type_poly_var. by apply: rt_refl. - move=> r ts IH t. rewrite [length _]/=. have ->: S (length ts) = (length ts) + 1 by lia. rewrite -many_poly_abs_many_poly_abs /=. have {}IH := IH (poly_abs t). apply: rt_trans; first by eassumption. apply: rt_step => /=. have := contains_step_subst. evar (s': poly_type) => /(_ s'). evar (t': poly_type) => /(_ t'). congr contains_step. subst t'. rewrite ?poly_type_norm /=. apply: ext_poly_type. case=> /=; first by subst s'. move=> ?. 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