Theorem: IntuitionisticPropositionalLogic.isTrue_equiv (GlimpseOfLean/Solutions/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v (A ⇔ B) = (eval v A ⇨ eval v B) ⊓ (eval v B ⇨ eval v A)
Tactic:
simp
State after:
no goals