proposition: Lemma typing_x_1_W : (forall Gamma, typing (many_poly_abs n_W' (poly_arr t_x_W' t_x_W') :: Gamma) x_1_W (poly_arr t_x_0_W t_x_0_W)).
proof: Proof. Proof using Hφψ0. move=> Gamma. rewrite /x_1_W. evar (t: poly_type). have := @typing_var (many_poly_abs n_W' (poly_arr t_x_W' t_x_W') :: Gamma) 0 t. subst t. move=> /(_ ltac:(reflexivity)) /typing_many_ty_appI => /(_ ts_1_W). apply: unnest. { by rewrite /ts_1_W map_length rev_length seq_length. } congr typing => /=. apply: poly_arr_eq_eq. rewrite /ts_1_W /t_x_W' /t_x_0_W -Hφψ0. rewrite -map_rev rev_involutive. apply: subst_poly_type_SU_term_to_poly_type. rewrite /n_W' /t_x_W' -lock /=. by lia. 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