Theorem: Sinf.succ_cong (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 =>
  constructor <;> try constructor <;> try assumption
  simp at *
  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:
constructor <;> try constructor <;> try assumption
State after:
case a
θ₁ θ₂ : Sinf_term
Δ : Ctx Sinf
nv₁ : NoVars θ₁
nv₂ : NoVars θ₂
e : Sinf_const.eval (Sinf_const.coerce θ₁ nv₁) = Sinf_const.eval (Sinf_const.coerce θ₂ nv₂)
⊢ Sinf_const.eval (Sinf_const.coerce (θ₁↗) (NoVars.S nv₁)) = Sinf_const.eval (Sinf_const.coerce (θ₂↗) (NoVars.S nv₂))

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

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

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

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

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