fact: 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.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics