Definition inv_equality_by_case_equality_by_case {A B : UU} {x y : A ⨿ B} (p : x = y) : @inv_equality_by_case A B x y (equality_by_case p) = p. Proof. induction x, y, p ; apply idpath. Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.