induction d
α : Type u_1
Δ : Sequent α
d :  ⊢¹ Δ
v : Valuation α
⊢ v ⊧ List.disj Δ
case axL
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
a✝ : α
⊢ v ⊧ (Formula.atom a✝ :: Formula.natom a✝ :: Δ✝).disj

case verum
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
⊢ v ⊧ (⊤ :: Δ✝).disj

case or
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝ : Derivation (p✝ :: q✝ :: Δ✝)
a_ih✝ : v ⊧ (p✝ :: q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋎ q✝ :: Δ✝).disj

case and
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ q✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (q✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (q✝ :: Δ✝).disj
⊢ v ⊧ (p✝ ⋏ q✝ :: Δ✝).disj

case wk
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ Γ✝ : Sequent α
a✝¹ : Derivation Δ✝
a✝ : Δ✝ ⊆ Γ✝
a_ih✝ : v ⊧ List.disj Δ✝
⊢ v ⊧ List.disj Γ✝

case cut
α : Type u_1
Δ : Sequent α
v : Valuation α
Δ✝ : List (Formula α)
p✝ : Formula α
a✝¹ : Derivation (p✝ :: Δ✝)
a✝ : Derivation (~p✝ :: Δ✝)
a_ih✝¹ : v ⊧ (p✝ :: Δ✝).disj
a_ih✝ : v ⊧ (~p✝ :: Δ✝).disj
⊢ v ⊧ Δ✝.disj