fact: Definition path_sum_inv {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.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall