proposition: Lemma aux_pure_typing_N0 {s n Gamma e }: is_simple s -> allfv_poly_type (gt (n+e)) s -> allfv_poly_type (fun x => nth_error Gamma x = Some (poly_var x)) (many_poly_abs n s) -> nth_error Gamma e = Some poly_abba -> pure_typing Gamma (many_pure_term_abs n (trace_poly_type (n+e) s)) (Nat.iter n (fun s' : poly_type => poly_abs (poly_arr (poly_var 0) s')) s).
proof: Proof. move=> Hs. elim: n Gamma e. - move=> Gamma e /= _. elim: s Gamma Hs. + move=> /= *. by apply: pure_typing_pure_var_simpleI. + move=> s IHs t IHt Gamma /= [/IHs {}IHs /IHt {}IHt] [/IHs {}IHs /IHt {}IHt]. move=> /[dup] [He] /[dup] [/IHs {}IHs /IHt {}IHt]. apply: (pure_typing_pure_app_simpleI (s := s)); last done. apply: (pure_typing_pure_app 0 (s := t)); rewrite ?map_ren_poly_type_id; last by apply: rt_refl. * apply: (pure_typing_pure_var 0); [by rewrite nth_error_map He | ]. apply: rt_trans; apply: rt_step. ** by apply: contains_stepI. ** apply: contains_stepI. by rewrite /= poly_type_norm /= subst_poly_type_poly_var. * done. + done. - move=> n IH Gamma e /= H1ns H2ns He. apply: (pure_typing_pure_abs 1). have ->: S (n + e) = n + S e by lia. apply: IH. + apply: allfv_poly_type_impl H1ns. by lia. + apply: allfv_poly_type_impl H2ns. case; first done. move=> ? /=. by rewrite nth_error_map => ->. + by rewrite /= nth_error_map He. 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 pure_typing_facts) ssreflect ssrbool ssrfun