Theorem: Sinf.succ_inj (SInfinity/Lemmas.lean)

State before:
⊢ ∀ {θ₁ θ₂ : Sinf_term} {Δ : Ctx Sinf}, Δ ⋁ θ₁↗ =ₛ θ₂↗ → Δ ⋁ θ₁ =ₛ θ₂
Tactic:
intros θ₁ θ₂ Δ _12
State after:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁↗ =ₛ θ₂↗
⊢ Δ ⋁ θ₁ =ₛ θ₂

State before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
_12 : Δ ⋁ θ₁↗ =ₛ θ₂↗
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases _12
State after:
case S_axiom
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁✝ : NoVars (θ₁↗)
nv₂✝ : NoVars (θ₂↗)
a✝ : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁✝) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂✝)
⊢ Δ ⋁ θ₁ =ₛ θ₂

case S_weakening
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
a✝ : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂

State before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars (θ₁↗)
nv₂ : NoVars (θ₂↗)
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
case S_axiom nv₁ nv₂ e =>
  cases nv₁; cases nv₂; constructor <;> try assumption
  simp at e
  assumption
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂
Tactic:
case S_weakening ne => exact (S_weakening (θ₁ =ₛ θ₂) ne)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars (θ₁↗)
nv₂ : NoVars (θ₂↗)
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) nv₁) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases nv₁
State after:
case S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₂ : NoVars (θ₂↗)
a✝ : NoVars θ₁
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂

State before:
case S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₂ : NoVars (θ₂↗)
a✝ : NoVars θ₁
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) nv₂)
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
cases nv₂
State after:
case S.S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Δ ⋁ θ₁ =ₛ θ₂

State before:
case S.S
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Δ ⋁ θ₁ =ₛ θ₂
Tactic:
constructor <;> try assumption
State after:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)

State before:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Tactic:
simp at e
State after:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)

State before:
case S.S.a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
⊢ Sinf_const.eval (Sinf_const.coerce θ₁ a✝¹) = Sinf_const.eval (Sinf_const.coerce θ₂ a✝)
Tactic:
assumption
State after:
no goals

State before:
case S.S.nv₂
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S a✝¹)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S a✝))
⊢ NoVars θ₂
Tactic:
assumption
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
δ✝ : Sinf
Δ✝ : Ctx Sinf
ne : Δ✝ ⋁ δ✝
⊢ δ✝ :: Δ✝ ⋁ θ₁ =ₛ θ₂
Tactic:
exact (S_weakening (θ₁ =ₛ θ₂) ne)
State after:
no goals