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