proposition: Lemma centralAllExOthBool `{Funext} (f: AllExistsOther Bool) : centerAllExOthBool = f.
proof: Proof. apply path_forall. intro b. pose proof (inverse (negb_ne (f b).2)) as fst. unfold centerAllExOthBool. apply (@path_sigma _ _ (negb b; not_fixed_negb b) (f b) fst); simpl. apply equiv_hprop_allpath. apply istrunc_forall. Defined.
imports: HoTT(Basics Types HProp HSet Projective TruncType Truncations Modalities.Notnot Modalities.Open Modalities.Closed BoundedSearch Equiv.BiInv Spaces.Nat Spaces.Torus.TorusEquivCircles Metatheory.Core Metatheory.FunextVarieties)