fact: Definition up_ren_ren_pure_term_pure_term (xi : ( nat ) -> nat ) (tau : ( nat ) -> nat ) (theta : ( nat ) -> nat ) (Eq : forall x, (funcomp tau xi) x = theta x) : forall x, (funcomp (upRen_pure_term_pure_term tau) (upRen_pure_term_pure_term xi)) x = (upRen_pure_term_pure_term theta) x := up_ren_ren xi tau theta Eq.
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms