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

State before:
p q : Prop
⊢ (p ∨ q) = (q ∨ p)
Tactic:
simp [or_comm]
State after:
no goals