proposition: Lemma equality_by_case_equiv {A B} (t u : A ⨿ B) : (t = u) ≃ equality_cases t u.
proof: Proof. use weq_iso. - apply equality_by_case. - apply inv_equality_by_case. - apply inv_equality_by_case_equality_by_case. - apply equality_by_case_inv_equality_by_case. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Tactics