case orI1 ih =>
  simp
  exact le_trans (ih hv) le_sup_left
H✝ : Type ?u.36751
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A B : Formula
Γ Δ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
ih : Γ✝ ⊨ A✝
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ✝, c ≤ eval v B
⊢ c ≤ eval v (A✝ || B✝)
no goals