induction h generalizing Δ
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Δ : Set Formula
h : Γ ⊢ A
h2 : Γ ⊆ Δ
⊢ Δ ⊢ A
case ax
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : A✝ ∈ Γ✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case impI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : insert A✝ Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ ⇒ B✝

case impE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝ ⇒ B✝
a✝ : Γ✝ ⊢ A✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ ⇒ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case andI
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝¹ : Γ✝ ⊢ A✝
a✝ : Γ✝ ⊢ B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ && B✝

case andE1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝

case andE2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝ && B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ && B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ B✝

case orI1
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ A✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orI2
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ : Formula
a✝ : Γ✝ ⊢ B✝
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ B✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝ || B✝

case orE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ B✝ C✝ : Formula
a✝² : Γ✝ ⊢ A✝ || B✝
a✝¹ : insert A✝ Γ✝ ⊢ C✝
a✝ : insert B✝ Γ✝ ⊢ C✝
a_ih✝² : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ A✝ || B✝
a_ih✝¹ : ∀ {Δ : Set Formula}, insert A✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
a_ih✝ : ∀ {Δ : Set Formula}, insert B✝ Γ✝ ⊆ Δ → Δ ⊢ C✝
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ C✝

case botE
H : Type ?u.100787
inst✝ : HeytingAlgebra H
v : Variable → H
A B : Formula
Γ Γ✝ : Set Formula
A✝ : Formula
a✝ : Γ✝ ⊢ bot
a_ih✝ : ∀ {Δ : Set Formula}, Γ✝ ⊆ Δ → Δ ⊢ bot
Δ : Set Formula
h2 : Γ✝ ⊆ Δ
⊢ Δ ⊢ A✝