Theorem: S_inl (SInfinity/Lemmas.lean)

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

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

State before:
case a
α β : Sinf
Δ : Ctx Sinf
a : Δ ⋁ α
⊢ Δ ⋁ β ∨ₛ α
Tactic:
exact (S_inr β a)
State after:
no goals