make the metric on types the expected one; define the old metric as another relation that's used only for constructing the fixpoint