Theorem: NoVars.unique (SInfinity/Basic.lean)

State before:
θ : Sinf_term
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
Tactic:
induction θ <;> try contradiction
State after:
case O
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂

case S
a✝ : Sinf_term
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝↗)
⊢ nv₁ = nv₂

case plus
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ +ₛ a✝)
⊢ nv₁ = nv₂

case times
a✝¹ a✝ : Sinf_term
a_ih✝¹ : ∀ (nv₁ nv₂ : NoVars a✝¹), nv₁ = nv₂
a_ih✝ : ∀ (nv₁ nv₂ : NoVars a✝), nv₁ = nv₂
nv₁ nv₂ : NoVars (a✝¹ *ₛ a✝)
⊢ nv₁ = nv₂

State before:
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂
Tactic:
case O => cases nv₁; cases nv₂; rfl
State after:
no goals

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ↗)
⊢ nv₁ = nv₂
Tactic:
case S θ ih =>
  cases nv₁; case S nv₁ => cases nv₂; case S nv₂ =>
  apply congrArg; exact (ih nv₁ nv₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ +ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
case plus θ₁ θ₂ ih₁ ih₂ =>
  cases nv₁; case plus nv₁₁ nv₂₁ => cases nv₂; case plus nv₁₂ nv₂₂ =>
  apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ *ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
case times θ₁ θ₂ ih₁ ih₂ =>
  cases nv₁; case times nv₁₁ nv₂₁ => cases nv₂; case times nv₁₂ nv₂₂ =>
  apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
case var
a✝ : String
nv₁ nv₂ : NoVars _ a✝
⊢ nv₁ = nv₂
Tactic:
contradiction
State after:
no goals

State before:
nv₁ nv₂ : NoVars Sinf_term.O
⊢ nv₁ = nv₂
Tactic:
cases nv₁
State after:
case O
nv₂ : NoVars Sinf_term.O
⊢ O = nv₂

State before:
case O
nv₂ : NoVars Sinf_term.O
⊢ O = nv₂
Tactic:
cases nv₂
State after:
case O.O

⊢ O = O

State before:
case O.O

⊢ O = O
Tactic:
rfl
State after:
no goals

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ↗)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
State after:
case S
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
a✝ : NoVars θ
⊢ S a✝ = nv₂

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
nv₁ : NoVars θ
⊢ S nv₁ = nv₂
Tactic:
case S nv₁ => cases nv₂; case S nv₂ =>
apply congrArg; exact (ih nv₁ nv₂)
State after:
no goals

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₂ : NoVars (θ↗)
nv₁ : NoVars θ
⊢ S nv₁ = nv₂
Tactic:
cases nv₂
State after:
case S
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ a✝ : NoVars θ
⊢ S nv₁ = S a✝

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ S nv₁ = S nv₂
Tactic:
case S nv₂ =>
apply congrArg; exact (ih nv₁ nv₂)
State after:
no goals

State before:
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ S nv₁ = S nv₂
Tactic:
apply congrArg
State after:
case h
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂

State before:
case h
θ : Sinf_term
ih : ∀ (nv₁ nv₂ : NoVars θ), nv₁ = nv₂
nv₁ nv₂ : NoVars θ
⊢ nv₁ = nv₂
Tactic:
exact (ih nv₁ nv₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ +ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
State after:
case plus
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ plus a✝¹ a✝ = nv₂

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = nv₂
Tactic:
case plus nv₁₁ nv₂₁ => cases nv₂; case plus nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ +ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = nv₂
Tactic:
cases nv₂
State after:
case plus
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus a✝¹ a✝

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus nv₁₂ nv₂₂
Tactic:
case plus nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ plus nv₁₁ nv₂₁ = plus nv₁₂ nv₂₂
Tactic:
apply congrArg₂
State after:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂

State before:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Tactic:
exact (ih₁ nv₁₁ nv₁₂)
State after:
case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂

State before:
case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂
Tactic:
exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁ nv₂ : NoVars (θ₁ *ₛ θ₂)
⊢ nv₁ = nv₂
Tactic:
cases nv₁
State after:
case times
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ times a✝¹ a✝ = nv₂

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = nv₂
Tactic:
case times nv₁₁ nv₂₁ => cases nv₂; case times nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₂ : NoVars (θ₁ *ₛ θ₂)
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = nv₂
Tactic:
cases nv₂
State after:
case times
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
a✝¹ : NoVars θ₁
a✝ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times a✝¹ a✝

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times nv₁₂ nv₂₂
Tactic:
case times nv₁₂ nv₂₂ =>
apply congrArg₂; exact (ih₁ nv₁₁ nv₁₂); exact (ih₂ nv₂₁ nv₂₂)
State after:
no goals

State before:
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ times nv₁₁ nv₂₁ = times nv₁₂ nv₂₂
Tactic:
apply congrArg₂
State after:
case hx
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₁₁ = nv₁₂

case hy
θ₁ θ₂ : Sinf_term
ih₁ : ∀ (nv₁ nv₂ : NoVars θ₁), nv₁ = nv₂
ih₂ : ∀ (nv₁ nv₂ : NoVars θ₂), nv₁ = nv₂
nv₁₁ : NoVars θ₁
nv₂₁ : NoVars θ₂
nv₁₂ : NoVars θ₁
nv₂₂ : NoVars θ₂
⊢ nv₂₁ = nv₂₂