fact: Definition up_term_term (sigma : ( nat ) -> term ) : ( nat ) -> term := scons ((var ) var_zero) (funcomp (ren_term id shift) sigma).
imports: Undecidability.SystemF.Autosubst.unscoped Undecidability.SystemF.SysF Morphisms