simp
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ ⇒ B✝)
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
ih : insert A✝ Γ✝ ⊨ B✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ⊓ eval v A✝ ≤ eval v B✝