for phi, psi being Ordinal-Sequence st rng phi = rng psi & phi is increasing & psi is increasing holds
phi = psi