{A B : Type} {z z' : A + B} (pq : z = z') : match z, z' with | inl z0, inl z'0 => z0 = z'0 | inr z0, inr z'0 => z0 = z'0 | _, _ => Empty end := match pq with | 1 => match z with | inl _ => 1 | inr _ => 1 end end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.