proposition: Lemma contains_sub {n s t t''} : contains (many_poly_abs n (poly_arr s t)) t'' -> exists n' s' t', 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. move Es1: (many_poly_abs n _) => s1 /clos_rt_rt1n_iff Hs1s2. elim: Hs1s2 n s t Es1. - move=> > <-. do 3 eexists. constructor; first done. constructor; by apply: rt_refl. - move=> > [] r > _ IH [|n] > /=; first done. move=> [] /(congr1 (subst_poly_type (r .: poly_var))). rewrite subst_poly_type_many_poly_abs /= => /IH [?] [?] [?] [->]. rewrite -?subst_poly_type_many_poly_abs => - [? ?]. do 3 eexists. constructor; first done. constructor; (apply: rt_trans; [| by eassumption]); by apply /rt_step. 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