proposition: Lemma contains_sub' {n s t n' s' t'} : contains (many_poly_abs n (poly_arr s t)) (many_poly_abs n' (poly_arr s' t')) -> contains (many_poly_abs n s) (many_poly_abs n' s') /\ contains (many_poly_abs n t) (many_poly_abs n' t').
proof: Proof. by move=> /contains_sub [?] [?] [?] [/many_poly_abs_eqE'] [<-] [<- <-]. 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