Theorem: FOL.NV.isAlphaEqvVarListId (FOL/NV/Alpha.lean)

State before:
xs : List VarName
⊢ isAlphaEqvVarList [] xs xs
Tactic:
induction xs
State after:
case nil

⊢ isAlphaEqvVarList [] [] []

case cons
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : isAlphaEqvVarList [] tail✝ tail✝
⊢ isAlphaEqvVarList [] (head✝ :: tail✝) (head✝ :: tail✝)

State before:
⊢ isAlphaEqvVarList [] [] []
Tactic:
case nil =>
  simp only [isAlphaEqvVarList]
State after:
no goals

State before:
⊢ isAlphaEqvVarList [] [] []
Tactic:
simp only [isAlphaEqvVarList]
State after:
no goals

State before:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] (hd :: tl) (hd :: tl)
Tactic:
simp only [isAlphaEqvVarList]
State after:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl

State before:
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd ∧ isAlphaEqvVarList [] tl tl
Tactic:
constructor
State after:
case left
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd

case right
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] tl tl

State before:
case left
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVar [] hd hd
Tactic:
simp only [isAlphaEqvVar]
State after:
no goals

State before:
case right
hd : VarName
tl : List VarName
ih : isAlphaEqvVarList [] tl tl
⊢ isAlphaEqvVarList [] tl tl
Tactic:
exact ih
State after:
no goals