proposition: Lemma typing_ren_poly_type {Gamma P t} ξ : typing Gamma P t -> typing (map (ren_poly_type ξ) Gamma) (ren_term ξ id P) (ren_poly_type ξ t).
proof: Proof. move=> /(typing_subst_poly_type (ξ >> poly_var)). congr typing. - apply: map_ext => ?. by rewrite -[RHS]subst_poly_type_poly_var ?poly_type_norm. - by rewrite -[RHS]subst_term_poly_var_var ?term_norm. - by rewrite -[RHS]subst_poly_type_poly_var ?poly_type_norm. Qed.
imports: List Lia Undecidability.SystemF.SysF Undecidability.SystemF.Autosubst.syntax Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.Util(Facts poly_type_facts term_facts) ssreflect ssrbool ssrfun