internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ (if x = h1_x then h1_d else h1_V x) = if y = h1_y then h1_d else h1_V' y
Tactic:
simp only [if_neg h2_left_left, if_neg h2_left_right]
Proof state after:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ h1_V x = h1_V' y
Theorem: FOL.NV.aux_1
Proof state before:
D : Type
binders : List (VarName × VarName)
x y : VarName
V V' : VarAssignment D
h1_l : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
a✝ : AlphaEqvVarAssignment D h1_l h1_V h1_V'
h1_ih : isAlphaEqvVar h1_l x y → h1_V x = h1_V' y
h2_right : isAlphaEqvVar h1_l x y
h2_left_left : ¬x = h1_x
h2_left_right : ¬y = h1_y
⊢ h1_V x = h1_V' y
Tactic:
exact h1_ih h2_right
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof 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✝)
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof 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✝)
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof 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)
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof 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
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.aux_2
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof state before:
binders : List (VarName × VarName)
xs ys : List VarName
h1 : isAlphaEqvVarList binders xs ys
⊢ xs.length = ys.length
Tactic:
induction xs generalizing ys
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof state before:
binders : List (VarName × VarName)
ys : List VarName
h1 : isAlphaEqvVarList binders [] ys
⊢ [].length = ys.length
Tactic:
cases ys
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof state before:
binders : List (VarName × VarName)
h1 : isAlphaEqvVarList binders [] []
⊢ [].length = [].length
Tactic:
case nil =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof state before:
binders : List (VarName × VarName)
h1 : isAlphaEqvVarList binders [] []
⊢ [].length = [].length
Tactic:
rfl
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof 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
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqvVarList_length
Proof 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
Proof state after:
no goals