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

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