fact: Definition up_ren_subst_term_term (xi : ( nat ) -> nat ) (tau : ( nat ) -> term ) (theta : ( nat ) -> term ) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (up_term_term tau) (upRen_term_term xi)) x = (up_term_term theta) x := fun n => match n with | S n => ap (ren_term id shift) (Eq n) | 0 => eq_refl end.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms