Theorem: Assignment.has_of_both (LeanSAT/LRAT/Assignment.lean)

State before:
b : Bool
⊢ hasAssignment b both = true
Tactic:
rw [hasAssignment]
State after:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true

State before:
b : Bool
⊢ (if b = true then hasPosAssignment else hasNegAssignment) both = true
Tactic:
split <;> decide
State after:
no goals