Theorem: S_inr (SInfinity/Lemmas.lean)

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

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

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

State before:
case a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ β :: Δ ⋁ α
Tactic:
apply S_weakening
State after:
case a.a.a
α β : Sinf
Δ : Ctx Sinf
b : Δ ⋁ β
⊢ Δ ⋁ β

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