Theorem: IntuitionisticPropositionalLogic.eval_top (GlimpseOfLean/Exercises/Topics/IntuitionisticPropositionalLogic.lean)

State before:
H : Type u_1
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
⊢ eval v top = ⊤
Tactic:
sorry
State after:
no goals