fact: Definition rinstInst_up_poly_type_poly_type (xi : ( nat ) -> nat ) (sigma : ( nat ) -> poly_type ) (Eq : forall x, (funcomp (poly_var ) xi) x = sigma x) : forall x, (funcomp (poly_var ) (upRen_poly_type_poly_type xi)) x = (up_poly_type_poly_type sigma) x := fun n => match n with | S n => ap (ren_poly_type shift) (Eq n) | 0 => eq_refl end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms