/-- Bool benchmark: double negation is identity for Bool. -/
theorem bool_not_not (b : Bool) : (!(!b)) = b := by
{{PROOF}}