fact: Definition nontrivial_qidem_baut_baut_bool : IsQuasiIdempotent (preidem_idmap (BAut (BAut Bool))) := negb_center2_baut_baut_bool.
imports: HoTT.Basics HoTT.Types Equiv.BiInv Idempotents Spaces.BAut Spaces.BAut.Bool