Update theories/Types/Bool.v

Alizter · jdchristensen · web-flow · commit bfb2b4013933 · 2024-05-04T15:25:59.000+01:00
Co-authored-by: Dan Christensen &lt;jdc+github@uwo.ca&gt;
diff --git a/theories/Types/Bool.v b/theories/Types/Bool.v
@@ -99,7 +99,7 @@ Proof.
   intros oops.
   symmetry.
   apply negb_ne.
-  intros p; symmetry in p; contradiction.
+  exact (symmetric_neq oops).
 Defined.
 
 (** ** Products as [forall] over [Bool] *)
