(negb_center_baut_bool pt)..1 = path_universe negb. Proof. apply moveL_equiv_V. apply negb_baut_bool_bool_negb. Defined.
Require Import HoTT.Basics HoTT.Types. Require Import Constant. Require Import HoTT.Truncations.Core HoTT.Truncations.Connectedness. Require Import Universes.BAut. Require Import Pointed.Core.