proposition: Lemma not_id_on_Bool `{Funext} : solution_6_9 Bool <> idmap.
proof: Proof. intro Bad. pose proof ((happly Bad) true) as Ugly. assert ((solution_6_9 Bool true) = false) as Good. - unfold solution_6_9. destruct (LEM (Contr (AllExistsOther Bool)) _) as [C|C];simpl. + elim (centralAllExOthBool (@center _ C)). reflexivity. + elim (C contrAllExOthBool). - apply false_ne_true. rewrite (inverse Good). assumption. 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)