Theorem: S_contraction (SInfinity/Lemmas.lean)

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

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

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

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