case impE ih₁ ih₂ =>
  specialize ih₁ hv
  simp at ih₁
  rwa [inf_eq_left.mpr (ih₂ hv)] at ih₁
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
ih₁ : Γ✝ ⊨ A✝ ⇒ B✝
ih₂ : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v B✝
no goals