Definition inv_equality_by_case {P Q : UU} {x x' : P ⨿ Q} : equality_cases x x' -> x = x'. Proof. intros e. induction x as [p|q]. - induction x' as [p'|q']. + exact (maponpaths (@ii1 P Q) e). + induction e. - induction x' as [p'|q']. + induction e. + exact (maponpaths (@ii2 P Q) e). Defined.