Theorem: S_dne (SInfinity/Lemmas.lean)

State before:
⊢ ∀ {α : Sinf} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ ¬ₛ α → Δ ⋁ α
Tactic:
intros α Δ dn
State after:
α : Sinf
Δ : Ctx Sinf
dn : Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ α

State before:
α : Sinf
Δ : Ctx Sinf
dn : Δ ⋁ ¬ₛ ¬ₛ α
⊢ Δ ⋁ α
Tactic:
cases dn
State after:
case S_weakening
α δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α

case S_dni
α : Sinf
Δ : Ctx Sinf
a✝ : Δ ⋁ α
⊢ Δ ⋁ α

State before:
α δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α
Tactic:
case S_weakening ne => exact (S_weakening α ne)
State after:
no goals

State before:
α : Sinf
Δ : Ctx Sinf
β : Δ ⋁ α
⊢ Δ ⋁ α
Tactic:
case S_dni β => exact β
State after:
no goals

State before:
α δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ α
Tactic:
exact (S_weakening α ne)
State after:
no goals

State before:
α : Sinf
Δ : Ctx Sinf
β : Δ ⋁ α
⊢ Δ ⋁ α
Tactic:
exact β
State after:
no goals