proposition: Lemma pure_typing_subst_poly_type {Gamma M t} σ : pure_typing Gamma M t -> pure_typing (map (subst_poly_type σ) Gamma) M (subst_poly_type σ t).
proof: Proof. pose σ' n σ := Nat.iter n up_poly_type_poly_type σ. have Hσ' : forall n t σ, subst_poly_type (σ' n σ) (ren_poly_type (Nat.add n) t) = ren_poly_type (Nat.add n) (subst_poly_type σ t). { move=> >. rewrite ?poly_type_norm /σ' /=. apply: ext_poly_type. move=> ?. by rewrite iter_up_poly_type_poly_type. } move=> H. elim: H σ. - move=> n {}Gamma x > Hx + σ => /(contains_subst_poly_typeI (σ' n σ)) HC. 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=> n > _ + _ + + σ => /(_ (σ' n σ)) + /(_ (σ' n σ)) + /(contains_subst_poly_typeI (σ' n σ)) ?. rewrite ?map_map. under map_ext => ? do rewrite Hσ'. move=> ? ?. rewrite subst_poly_type_many_poly_abs. apply: (pure_typing_pure_app n); rewrite ?map_map; by eassumption. - move=> n > _ + σ => /(_ (σ' n σ)). rewrite /= map_map. under map_ext => ? do rewrite Hσ'. move=> ?. rewrite subst_poly_type_many_poly_abs /=. apply: (pure_typing_pure_abs n). rewrite ?map_map. by eassumption. 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