proposition: Lemma typing_Q_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)) -> (forall Gamma, typing (many_poly_abs n_W' (poly_arr t_x_W' t_x_W') :: Gamma) x_2_W (poly_arr t_x_1_W t_x_1_W)) -> typing Gamma_W Q_W (poly_arr t_x_W t_x_W).
proof: Proof. move=> H1 H2. apply /typing_abs /typing_many_ty_absI. apply: (typing_app (s := (poly_arr t_x_1_W t_x_1_W))); [apply: (typing_app (s := (poly_arr t_x_0_W t_x_0_W))) |]. - evar (t : poly_type). have := @typing_var (map (ren_poly_type (Nat.add n_W')) (t_x_W :: Gamma_W)) 2 t. subst t. move=> /(_ ltac:(reflexivity)). rewrite ren_poly_type_many_poly_abs. move /typing_many_ty_appI => /(_ ts_0_W). apply: unnest. { by rewrite /ts_0_W map_length rev_length seq_length. } congr typing. rewrite /t_1_W /= -map_rev rev_involutive. congr poly_arr; [| congr poly_arr]; apply: poly_arr_eq_eq. + have := poly_var_bound_SUt0'_n_W. rewrite /t_x_0_W /SUt0' /ts_0_W. move=> ?. rewrite ren_poly_type_poly_var_bound; first by lia. by apply: subst_poly_type_SU_term_to_poly_type. + have := poly_var_bound_SUt1'_n_W. rewrite /t_x_1_W /SUt1' /ts_0_W. move=> ?. rewrite ren_poly_type_poly_var_bound; first by lia. by apply: subst_poly_type_SU_term_to_poly_type. + have := poly_var_bound_SUs'_n_W. rewrite /t_x_W' /SUs' /ts_0_W. move=> ?. rewrite ren_poly_type_poly_var_bound; first by lia. by apply: subst_poly_type_SU_term_to_poly_type. - rewrite /(map _ (_ :: _)) -/(map _ _). move: (map _ Gamma_W) => Gamma. rewrite /t_x_W ren_poly_type_many_poly_abs ren_poly_type_poly_var_bound; first by (rewrite /n_W' -lock /=; lia). by apply: H1. - rewrite /(map _ (_ :: _)) -/(map _ _). move: (map _ Gamma_W) => Gamma. rewrite /t_x_W ren_poly_type_many_poly_abs ren_poly_type_poly_var_bound; first by (rewrite /n_W' -lock /=; lia). by apply: H2. 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