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

State before:
D : Type
binders : List (VarName × VarName)
xs ys : List VarName
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVarList binders xs ys
⊢ List.map V xs = List.map V' ys
Tactic:
induction xs generalizing ys
State after:
case nil
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2 : isAlphaEqvVarList binders [] ys
⊢ List.map V [] = List.map V' ys

case cons
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
head✝ : VarName
tail✝ : List VarName
tail_ih✝ : ∀ (ys : List VarName), isAlphaEqvVarList binders tail✝ ys → List.map V tail✝ = List.map V' ys
ys : List VarName
h2 : isAlphaEqvVarList binders (head✝ :: tail✝) ys
⊢ List.map V (head✝ :: tail✝) = List.map V' ys

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2 : isAlphaEqvVarList binders [] ys
⊢ List.map V [] = List.map V' ys
Tactic:
case nil =>
  cases ys
  case nil =>
    simp
  case cons ys_hd ys_tl =>
    simp only [isAlphaEqvVarList] at h2
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys : List VarName
h2 : isAlphaEqvVarList binders [] ys
⊢ List.map V [] = List.map V' ys
Tactic:
cases ys
State after:
case nil
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVarList binders [] []
⊢ List.map V [] = List.map V' []

case cons
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
head✝ : VarName
tail✝ : List VarName
h2 : isAlphaEqvVarList binders [] (head✝ :: tail✝)
⊢ List.map V [] = List.map V' (head✝ :: tail✝)

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVarList binders [] []
⊢ List.map V [] = List.map V' []
Tactic:
case nil =>
  simp
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ List.map V [] = List.map V' (ys_hd :: ys_tl)
Tactic:
case cons ys_hd ys_tl =>
  simp only [isAlphaEqvVarList] at h2
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvVarList binders [] []
⊢ List.map V [] = List.map V' []
Tactic:
simp
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVarList binders [] (ys_hd :: ys_tl)
⊢ List.map V [] = List.map V' (ys_hd :: ys_tl)
Tactic:
simp only [isAlphaEqvVarList] at h2
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys : List VarName
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) ys
⊢ List.map V (xs_hd :: xs_tl) = List.map V' ys
Tactic:
cases ys
State after:
case nil
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ List.map V (xs_hd :: xs_tl) = List.map V' []

case cons
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
head✝ : VarName
tail✝ : List VarName
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (head✝ :: tail✝)
⊢ List.map V (xs_hd :: xs_tl) = List.map V' (head✝ :: tail✝)

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ List.map V (xs_hd :: xs_tl) = List.map V' []
Tactic:
case nil =>
  simp only [isAlphaEqvVarList] at h2
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) []
⊢ List.map V (xs_hd :: xs_tl) = List.map V' []
Tactic:
simp only [isAlphaEqvVarList] at h2
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVarList binders (xs_hd :: xs_tl) (ys_hd :: ys_tl)
⊢ List.map V (xs_hd :: xs_tl) = List.map V' (ys_hd :: ys_tl)
Tactic:
simp only [isAlphaEqvVarList] at h2
State after:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ List.map V (xs_hd :: xs_tl) = List.map V' (ys_hd :: ys_tl)

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ List.map V (xs_hd :: xs_tl) = List.map V' (ys_hd :: ys_tl)
Tactic:
simp
State after:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd ∧ List.map V xs_tl = List.map V' ys_tl

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd ∧ List.map V xs_tl = List.map V' ys_tl
Tactic:
constructor
State after:
case left
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd

case right
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ List.map V xs_tl = List.map V' ys_tl

State before:
case left
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd
Tactic:
cases h2
State after:
case left.intro
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
left✝ : isAlphaEqvVar binders xs_hd ys_hd
right✝ : isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2_left : isAlphaEqvVar binders xs_hd ys_hd
h2_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd
Tactic:
case left.intro h2_left h2_right =>
  exact aux_1 D binders xs_hd ys_hd V V' h1 h2_left
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2_left : isAlphaEqvVar binders xs_hd ys_hd
h2_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ V xs_hd = V' ys_hd
Tactic:
exact aux_1 D binders xs_hd ys_hd V V' h1 h2_left
State after:
no goals

State before:
case right
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ List.map V xs_tl = List.map V' ys_tl
Tactic:
apply xs_ih ys_tl
State after:
case right
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ isAlphaEqvVarList binders xs_tl ys_tl

State before:
case right
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2 : isAlphaEqvVar binders xs_hd ys_hd ∧ isAlphaEqvVarList binders xs_tl ys_tl
⊢ isAlphaEqvVarList binders xs_tl ys_tl
Tactic:
cases h2
State after:
case right.intro
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
left✝ : isAlphaEqvVar binders xs_hd ys_hd
right✝ : isAlphaEqvVarList binders xs_tl ys_tl
⊢ isAlphaEqvVarList binders xs_tl ys_tl

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2_left : isAlphaEqvVar binders xs_hd ys_hd
h2_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ isAlphaEqvVarList binders xs_tl ys_tl
Tactic:
case right.intro h2_left h2_right =>
  exact h2_right
State after:
no goals

State before:
D : Type
binders : List (VarName × VarName)
V V' : VarAssignment D
h1 : AlphaEqvVarAssignment D binders V V'
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → List.map V xs_tl = List.map V' ys
ys_hd : VarName
ys_tl : List VarName
h2_left : isAlphaEqvVar binders xs_hd ys_hd
h2_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ isAlphaEqvVarList binders xs_tl ys_tl
Tactic:
exact h2_right
State after:
no goals