simp
case h3v
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ D ∈ insert B Γ, c ⊓ eval v B ≤ eval v D
case h3v
H✝ : Type ?u.104354
inst✝ : HeytingAlgebra H✝
v✝ : Variable → H✝
A✝ B✝ : Formula
Γ✝ Δ Γ : Set Formula
A B C : Formula
_h1 : Γ ⊢ A || B
_h2 : insert A Γ ⊢ C
_h3 : insert B Γ ⊢ C
ih₂ : insert A Γ ⊨ C
ih₃ : insert B Γ ⊨ C
H : Type
hH : HeytingAlgebra H
v : Variable → H
c : H
hv : ∀ B ∈ Γ, c ≤ eval v B
ih₁ : c ≤ eval v (A || B)
h2v : ∀ D ∈ insert A Γ, c ⊓ eval v A ≤ eval v D
⊢ ∀ a ∈ Γ, c ⊓ eval v B ≤ eval v a