proposition: Lemma contains_subst_poly_typeI σ {s t} : contains s t -> contains (subst_poly_type σ s) (subst_poly_type σ t).
proof: Proof. elim. - move=> > [] > /=. apply: rt_step. rewrite poly_type_norm /=. 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. subst s'. case; first done. move=> ?. by rewrite /= poly_type_norm /= subst_poly_type_poly_var. - move=> ?. by apply: rt_refl. - move=> *. apply: rt_trans; by eassumption. 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