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

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