fact: Definition upExt_term_poly_type (sigma : ( nat ) -> poly_type ) (tau : ( nat ) -> poly_type ) (Eq : forall x, sigma x = tau x) : forall x, (up_term_poly_type sigma) x = (up_term_poly_type tau) x := fun n => ap (ren_poly_type id) (Eq n).
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms