proposition: Lemma decompose_N_W {s} : pure_typing Gamma_W N_W (poly_arr s s) -> exists n σ, s = many_poly_abs n (subst_poly_type σ (poly_arr SUs' SUs')) /\ pure_typing (map (ren_poly_type (Nat.add n)) (s :: Gamma_W)) (pure_var 0) (subst_poly_type σ (poly_arr SUt0' SUt0')) /\ pure_typing (map (ren_poly_type (Nat.add n)) (s :: Gamma_W)) (pure_var 0) (subst_poly_type σ (poly_arr SUt1' SUt1')).
proof: Proof. move=> /pure_typingE' /=. move=> /pure_typingE /= [n1] [?] [?] [?] [+] [+] [H1C ?]. move=> /pure_typingE' [?] [?] [+] [+ H2C]. move=> /pure_typingE' [?] [[?]] H3C. subst. move=> H1 H2. move: H3C. rewrite ren_poly_type_many_poly_abs /t_1_W /=. move=> /contains_poly_arrE [?] [?] [? ?]. subst. move: H2C => /containsE [? ?]. subst. move: H1C => /containsE ?. subst. do 2 eexists. constructor; first by rewrite ?poly_type_norm. constructor; [move: H1 | move: H2]; by rewrite ?poly_type_norm. 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