Theorem: Smt.Reconstruct.Prop.or_assoc_eq (Smt/Reconstruct/Prop/Core.lean)

State before:
a b c : Prop
⊢ ((a ∨ b) ∨ c) = (a ∨ b ∨ c)
Tactic:
simp [or_assoc]
State after:
no goals