proposition: Theorem Book_1_12_part3 : forall A B, ((~A) + (~B)) -> ~(A * B).
proof: Proof. intros A B [na | nb] [a b]. - exact (na a). - exact (nb b). Qed.
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)