proposition: Lemma decompose_x_W {n σ Gamma s' t'} : let s := many_poly_abs n (subst_poly_type σ (poly_arr s' s')) in pure_typing ((ren_poly_type (Nat.add n) s) :: Gamma) (pure_var 0) (subst_poly_type σ (poly_arr t' t')) -> exists τ, subst_poly_type (funcomp (subst_poly_type τ) σ) s' = subst_poly_type σ t'.
proof: Proof. move=> /= /pure_typingE' /= [?] [[?]]. subst. rewrite ren_poly_type_many_poly_abs /=. move=> /contains_poly_arrE [?] [?] [-> _]. rewrite ?poly_type_norm. by eexists. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Util(Facts poly_type_facts pure_term_facts term_facts typing_facts pure_typing_facts pure_typable_prenex) ssreflect ssrbool ssrfun