proposition: Lemma contains_subst_poly_type_fold_rightE {ts t t'} : contains (subst_poly_type (fold_right scons poly_var ts) t) t' -> contains (many_poly_abs (length ts) t) t'.
proof: Proof. move Hs: (subst_poly_type (fold_right scons poly_var ts) t) => s /clos_rt_rtn1_iff Hst'. elim: Hst' t ts Hs. - move=> ? ? <-. by apply: contains_subst_poly_type_fold_rightI. - move=> > [] r ? _ IH t ts /IH {}IH. apply: rt_trans; first by eassumption. by apply /rt_step /contains_step_subst. 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