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

State before:
binders : List (VarName × VarName)
xs ys : List VarName
h1 : isAlphaEqvVarList binders xs ys
⊢ xs.length = ys.length
Tactic:
induction xs generalizing ys
State after:
case nil
binders : List (VarName × VarName)
ys : List VarName
h1 : isAlphaEqvVarList binders [] ys
⊢ [].length = ys.length

case cons
binders : List (VarName × VarName)
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : ∀ (ys : List VarName), isAlphaEqvVarList binders tail✝ ys → tail✝.length = ys.length
ys : List VarName
h1 : isAlphaEqvVarList binders (head✝ :: tail✝) ys
⊢ (head✝ :: tail✝).length = ys.length

State before:
binders : List (VarName × VarName)
ys : List VarName
h1 : isAlphaEqvVarList binders [] ys
⊢ [].length = ys.length
Tactic:
case nil =>
  cases ys
  case nil =>
    rfl
  case cons ys_hd ys_tl =>
    simp only [isAlphaEqvVarList] at h1
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) ys
⊢ (xs_hd :: xs_tl).length = ys.length
Tactic:
case cons xs_hd xs_tl xs_ih =>
  cases ys
  case nil =>
    simp only [isAlphaEqvVarList] at h1
  case cons ys_hd ys_tl =>
    simp only [isAlphaEqvVarList] at h1
    simp
    cases h1
    case intro h1_left h1_right =>
      exact xs_ih ys_tl h1_right
State after:
no goals

State before:
binders : List (VarName × VarName)
ys : List VarName
h1 : isAlphaEqvVarList binders [] ys
⊢ [].length = ys.length
Tactic:
cases ys
State after:
case nil
binders : List (VarName × VarName)
h1 : isAlphaEqvVarList binders [] []
⊢ [].length = [].length

case cons
binders : List (VarName × VarName)
head✝ : VarName
tail✝ : List VarName
h1 : isAlphaEqvVarList binders [] (head✝ :: tail✝)
⊢ [].length = (head✝ :: tail✝).length

State before:
binders : List (VarName × VarName)
h1 : isAlphaEqvVarList binders [] []
⊢ [].length = [].length
Tactic:
case nil =>
  rfl
State after:
no goals

State before:
binders : List (VarName × VarName)
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ [].length = (ys_hd :: ys_tl).length
Tactic:
case cons ys_hd ys_tl =>
  simp only [isAlphaEqvVarList] at h1
State after:
no goals

State before:
binders : List (VarName × VarName)
h1 : isAlphaEqvVarList binders [] []
⊢ [].length = [].length
Tactic:
rfl
State after:
no goals

State before:
binders : List (VarName × VarName)
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ [].length = (ys_hd :: ys_tl).length
Tactic:
simp only [isAlphaEqvVarList] at h1
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) ys
⊢ (xs_hd :: xs_tl).length = ys.length
Tactic:
cases ys
State after:
case nil
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ (xs_hd :: xs_tl).length = [].length

case cons
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
head✝ : VarName
tail✝ : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (head✝ :: tail✝)
⊢ (xs_hd :: xs_tl).length = (head✝ :: tail✝).length

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ (xs_hd :: xs_tl).length = [].length
Tactic:
case nil =>
  simp only [isAlphaEqvVarList] at h1
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (ys_hd :: ys_tl)
⊢ (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
Tactic:
case cons ys_hd ys_tl =>
  simp only [isAlphaEqvVarList] at h1
  simp
  cases h1
  case intro h1_left h1_right =>
    exact xs_ih ys_tl h1_right
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ (xs_hd :: xs_tl).length = [].length
Tactic:
simp only [isAlphaEqvVarList] at h1
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (ys_hd :: ys_tl)
⊢ (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
Tactic:
simp only [isAlphaEqvVarList] at h1
State after:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ (xs_hd :: xs_tl).length = (ys_hd :: ys_tl).length
Tactic:
simp
State after:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length
Tactic:
cases h1
State after:
case intro
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
left✝ : isAlphaEqvVar binders xs_hd ys_hd
right✝ : isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1_left : isAlphaEqvVar binders xs_hd ys_hd
h1_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length
Tactic:
case intro h1_left h1_right =>
  exact xs_ih ys_tl h1_right
State after:
no goals

State before:
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1_left : isAlphaEqvVar binders xs_hd ys_hd
h1_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length
Tactic:
exact xs_ih ys_tl h1_right
State after:
no goals