Theorem: S_neg_forall_inv (SInfinity/Lemmas.lean)

State before:
⊢ ∀ {α : Sinf} {x : String} {Δ : Ctx Sinf}, Δ ⋁ ¬ₛ (∀ₛ x ; α) → ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
intros α x Δ nf
State after:
α : Sinf
x : String
Δ : Ctx Sinf
nf : Δ ⋁ ¬ₛ (∀ₛ x ; α)
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]

State before:
α : Sinf
x : String
Δ : Ctx Sinf
nf : Δ ⋁ ¬ₛ (∀ₛ x ; α)
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
cases nf
State after:
case S_weakening
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]

case S_neg_forall
α : Sinf
x : String
Δ : Ctx Sinf
θ✝ : Sinf_term
a✝ : Δ ⋁ ¬ₛ α [x ≔ θ✝]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
case S_weakening ne => exists (_ x); exact (S_weakening (¬ₛ α[x ≔ _ x]) ne)
State after:
no goals

State before:
α : Sinf
x : String
Δ : Ctx Sinf
θ : Sinf_term
β : Δ ⋁ ¬ₛ α [x ≔ θ]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
case S_neg_forall θ β => exists θ
State after:
no goals

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ ∃ θ, δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
exists (_ x)
State after:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ _ x]

State before:
α : Sinf
x : String
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ ¬ₛ α [x ≔ _ x]
Tactic:
exact (S_weakening (¬ₛ α[x ≔ _ x]) ne)
State after:
no goals

State before:
α : Sinf
x : String
Δ : Ctx Sinf
θ : Sinf_term
β : Δ ⋁ ¬ₛ α [x ≔ θ]
⊢ ∃ θ, Δ ⋁ ¬ₛ α [x ≔ θ]
Tactic:
exists θ
State after:
no goals