proposition: Lemma pure_typing_poly_absE {s Gamma M t} : pure_typing Gamma M (poly_abs t) -> pure_typing Gamma M (subst_poly_type (s .: poly_var) t).
proof: Proof. pose σ n s := Nat.iter n up_poly_type_poly_type (s .: poly_var). have Hσ: forall n t s, subst_poly_type (σ n s) (ren_poly_type (Nat.add (S n)) t) = ren_poly_type (Nat.add n) t. { move=> n >. rewrite ?poly_type_norm [RHS]ren_as_subst_poly_type /σ. apply: ext_poly_type => y /=. rewrite iter_up_poly_type_poly_type_ge; first by lia. by have ->: S (n + y) - n = S y by lia. } elim: M s Gamma t. - move=> x s Gamma t /pure_typingE [[|n]] [tx] [?] [+] [+] /=. + move=> *. subst. apply: (pure_typing_pure_var 0); first by eassumption. apply: rt_trans; [by eassumption | by apply /rt_step /contains_step_subst]. + move=> Hx /(contains_subst_poly_typeI (σ n s)) HC [?]. subst. rewrite subst_poly_type_many_poly_abs. apply: (pure_typing_pure_var n); last by eassumption. move: Hx. rewrite ?nth_error_map. case: (nth_error Gamma x); last done. move=> ? /= [<-]. by rewrite Hσ. - move=> ? IH1 ? IH2 s Gamma t /pure_typingE [[|n]] [?] [?] [?] [+] [+] []. + move=> ? ? ? /= ?. subst. apply: (pure_typing_pure_app 0); [by eassumption | by eassumption |]. apply: rt_trans; [by eassumption | by apply /rt_step /contains_step_subst]. + move=> /(pure_typing_subst_poly_type (σ n s)) /= + /(pure_typing_subst_poly_type (σ n s)) /= +. rewrite ?map_map. under map_ext => ? do rewrite Hσ. move=> ? ?. move=> /(contains_subst_poly_typeI (σ n s)) ? [->]. rewrite subst_poly_type_many_poly_abs. apply: (pure_typing_pure_app n); by eassumption. - move=> ? IH s Gamma t /pure_typingE [[|n]] [?] [?] []; first done. move=> + [->]. rewrite subst_poly_type_many_poly_abs. move=> /(pure_typing_subst_poly_type (σ n s)) /=. rewrite ?map_map. under map_ext => ? do rewrite Hσ. move=> ?. by apply: (pure_typing_pure_abs n). 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) ssreflect ssrbool ssrfun