Theorem: S_exchange (SInfinity/Lemmas.lean)

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

State before:
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ β ∨ₛ α
Tactic:
apply S_out
State after:
case a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ β :: Δ ⋁ α

State before:
case a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ β :: Δ ⋁ α
Tactic:
apply S_exchange_ctx
State after:
case a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ α :: Δ ⋁ β

State before:
case a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ α :: Δ ⋁ β
Tactic:
apply S_in
State after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ α ∨ₛ β

State before:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
αβ : Δ ⋁ α ∨ₛ β
⊢ Δ ⋁ α ∨ₛ β
Tactic:
assumption
State after:
no goals