If you generalize over the o \in u in the if condition, the erefl has type o \in u = o \in u where it needs to have type o \in u = x (with x the thing o \in u gets generalized to), so you need to generalize over erefl first.