{b1 b2 : Bool} : (b1 <> b2) -> (b1 = negb b2). Proof. destruct b1, b2. - intros oops; case (oops idpath). - reflexivity. - reflexivity. - intros oops; case (oops idpath). Defined.
Require Import HoTT.Basics. Require Import Types.Equiv.