~ (s o r == idmap). Proof. intros oops. assert (p := oops nontrivial_qidem_baut_baut_bool). assert (q := oops (isqidem_idmap (BAut (BAut Bool)))); clear oops. apply nontrivial_negb_center_baut_baut_bool. refine (p^ @ ap s _ @ q). pose (contr_splitting_preidem_idmap (BAut (BAut Bool))). apply path_contr. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Equiv.BiInv Idempotents. Require Import Universes.BAut Spaces.BAut.Bool.