(A : Type) {B : Type} {x x' : B} : inr x = inr x' -> x = x' := fun p => @path_sum_inv A B _ _ p.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.