Theorem: S_induction_inv (SInfinity/Lemmas.lean)

State before:
⊢ ∀ {α : Sinf} {x : String} {Δ : Ctx Sinf}, Δ ⋁ ∀ₛ x ; α → ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
intros α x Δ f
State after:
α : Sinf
x : String
Δ : Ctx Sinf
f : Δ ⋁ ∀ₛ x ; α
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]

State before:
α : Sinf
x : String
Δ : Ctx Sinf
f : Δ ⋁ ∀ₛ x ; α
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
cases f
State after:
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]

case S_induction
α : Sinf
x : String
Δ : Ctx Sinf
a✝ : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
case S_weakening ne => intros n; exact (S_weakening (α [x ≔ n]) ne)
State after:
no goals

State before:
α : Sinf
x : String
Δ : Ctx Sinf
i : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
case S_induction i => assumption
State after:
no goals

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∀ (n : ℕ), δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
intros n
State after:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
n : ℕ
⊢ δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
n : ℕ
⊢ δ✝ :: Δ✝ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
exact (S_weakening (α [x ≔ n]) ne)
State after:
no goals

State before:
α : Sinf
x : String
Δ : Ctx Sinf
i : ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
⊢ ∀ (n : ℕ), Δ ⋁ α [x ≔ Sinf_term.fromNat n]
Tactic:
assumption
State after:
no goals