Theorem: A3 (Bml/Examples.lean)

State before:
X Y : Formula
⊢ Tautology (□(X⋀Y)↣□X⋀□Y)
Tactic:
simp_all [Tautology, Evaluate]
State after:
no goals