Theorem: addition (Test/Bool/Addition.lean)

State before:
p q : Bool
⊢ p = true → (p || q) = true
Tactic:
simp_all
State after:
no goals