internlm/Lean-Github huggingface dataset:
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi → Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔
    Holds D I V (Formula.openList j (List.map free_ zs) phi) → Holds D I V (Formula.openList j (List.map free_ zs) psi)
Tactic:
congr! 1
Proof state after:
case a.h.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)

case a.h'.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
a✝ : Holds D I V (Formula.openList j (List.map free_ zs) phi)
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
Theorem: LN.HoldsOpenList
Proof state before:
case a.h.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
case a.h'.a
D : Type
I : Interpretation D
zs : List String
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
V : VarAssignment D
j : ℕ
a✝ : Holds D I V (Formula.openList j (List.map free_ zs) phi)
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) psi ↔ Holds D I V (Formula.openList j (List.map free_ zs) psi)
Tactic:
apply psi_ih
Proof state after:
no goals
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝ phi) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝ phi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ (∀ (d : D), Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi) ↔
    ∀ (d : D), Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Theorem: LN.HoldsOpenList
Proof state before:
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ (∀ (d : D), Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi) ↔
    ∀ (d : D), Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ∀ (a : D),
    Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) a) phi ↔
      Holds D I (shift D V a) (Formula.openList (j + 1) (List.map free_ zs) phi)
Theorem: LN.HoldsOpenList
Proof state before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
⊢ ∀ (a : D),
    Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) a) phi ↔
      Holds D I (shift D V a) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Theorem: LN.HoldsOpenList
Proof state before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d) (Formula.openList (j + 1) (List.map free_ zs) phi)
Tactic:
simp only [← phi_ih]
Proof state after:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) phi
Theorem: LN.HoldsOpenList
Proof state before:
case h
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ Holds D I (shift D (V ∘ Var.openList j (List.map free_ zs)) d) phi ↔
    Holds D I (shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)) phi
Tactic:
congr!
Proof state after:
case h.a.h.e'_3
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)
Theorem: LN.HoldsOpenList
Proof state before:
case h.a.h.e'_3
D : Type
I : Interpretation D
zs : List String
a✝ : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) phi ↔ Holds D I V (Formula.openList j (List.map free_ zs) phi)
V : VarAssignment D
j : ℕ
d : D
⊢ shift D (V ∘ Var.openList j (List.map free_ zs)) d = shift D V d ∘ Var.openList (j + 1) (List.map free_ zs)
Tactic:
apply ShiftVarOpenList
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
xs : List String
⊢ V ∘ Var.openList 0 (List.map free_ xs) = shiftList D V (List.map (V ∘ free_) xs)
Tactic:
induction xs
Proof state after:
case nil
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])

case cons
D : Type
V : VarAssignment D
head✝ : String
tail✝ : List String
tail_ih✝ : V ∘ Var.openList 0 (List.map free_ tail✝) = shiftList D V (List.map (V ∘ free_) tail✝)
⊢ V ∘ Var.openList 0 (List.map free_ (head✝ :: tail✝)) = shiftList D V (List.map (V ∘ free_) (head✝ :: tail✝))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
Tactic:
case nil =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [Var.openList]
  case _ i =>
    simp only [Var.openList]
    split
    case _ c1 =>
      rfl
    case _ c1 =>
      simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V ∘ Var.openList 0 (List.map free_ (hd :: tl)) = shiftList D V (List.map (V ∘ free_) (hd :: tl))
Tactic:
case _ hd tl ih =>
  funext v
  simp
  simp only [shiftList]
  cases v
  case _ x =>
    simp only [shift]
    simp only [← ih]
    simp only [Var.openList]
    simp
  case _ i =>
    cases i
    case zero =>
      simp only [shift]
      simp only [Var.openList]
      simp
    case succ i =>
      simp only [shift]
      simp only [← ih]
      simp
      simp only [Var.openList]
      simp
      split
      case _ c1 =>
        have s1 : i < tl.length
        linarith
        simp only [s1]
        simp
      case _ c1 =>
        have s1 : ¬ i < tl.length
        linarith
        simp only [s1]
        simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
⊢ V ∘ Var.openList 0 (List.map free_ []) = shiftList D V (List.map (V ∘ free_) [])
Tactic:
funext v
Proof state after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ [])) v = shiftList D V (List.map (V ∘ free_) []) v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ [])) v = shiftList D V (List.map (V ∘ free_) []) v
Tactic:
simp
Proof state after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = shiftList D V [] v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = shiftList D V [] v
Tactic:
simp only [shiftList]
Proof state after:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = V v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
v : Var
⊢ V (Var.openList 0 [] v) = V v
Tactic:
cases v
Proof state after:
case h.free_
D : Type
V : VarAssignment D
a✝ : String
⊢ V (Var.openList 0 [] (free_ a✝)) = V (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
a✝ : ℕ
⊢ V (Var.openList 0 [] (bound_ a✝)) = V (bound_ a✝)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
x : String
⊢ V (Var.openList 0 [] (free_ x)) = V (free_ x)
Tactic:
case _ x =>
  simp only [Var.openList]
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (Var.openList 0 [] (bound_ i)) = V (bound_ i)
Tactic:
case _ i =>
  simp only [Var.openList]
  split
  case _ c1 =>
    rfl
  case _ c1 =>
    simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
x : String
⊢ V (Var.openList 0 [] (free_ x)) = V (free_ x)
Tactic:
simp only [Var.openList]
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (Var.openList 0 [] (bound_ i)) = V (bound_ i)
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (if i < 0 then bound_ i else if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) =
    V (bound_ i)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
⊢ V (if i < 0 then bound_ i else if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) =
    V (bound_ i)
Tactic:
split
Proof state after:
case inl
D : Type
V : VarAssignment D
i : ℕ
h✝ : i < 0
⊢ V (bound_ i) = V (bound_ i)

case inr
D : Type
V : VarAssignment D
i : ℕ
h✝ : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
c1 : i < 0
⊢ V (bound_ i) = V (bound_ i)
Tactic:
case _ c1 =>
  rfl
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
c1 : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)
Tactic:
case _ c1 =>
  simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
c1 : i < 0
⊢ V (bound_ i) = V (bound_ i)
Tactic:
rfl
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
i : ℕ
c1 : ¬i < 0
⊢ V (if x : i - 0 < [].length then [][i - 0] else bound_ (i - 0 - [].length + 0)) = V (bound_ i)
Tactic:
simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V ∘ Var.openList 0 (List.map free_ (hd :: tl)) = shiftList D V (List.map (V ∘ free_) (hd :: tl))
Tactic:
funext v
Proof state after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ (hd :: tl))) v = shiftList D V (List.map (V ∘ free_) (hd :: tl)) v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ (V ∘ Var.openList 0 (List.map free_ (hd :: tl))) v = shiftList D V (List.map (V ∘ free_) (hd :: tl)) v
Tactic:
simp
Proof state after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) = shiftList D V (V (free_ hd) :: List.map (V ∘ free_) tl) v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) = shiftList D V (V (free_ hd) :: List.map (V ∘ free_) tl) v
Tactic:
simp only [shiftList]
Proof state after:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) v
Theorem: LN.ShiftListVarOpenList
Proof state before:
case h
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
v : Var
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) v) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) v
Tactic:
cases v
Proof state after:
case h.free_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ a✝)

case h.bound_
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
a✝ : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ a✝)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ a✝)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ x)
Tactic:
case _ x =>
  simp only [shift]
  simp only [← ih]
  simp only [Var.openList]
  simp
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = V (Var.openList 0 (List.map free_ tl) (free_ x))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ i)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ i)
Tactic:
case _ i =>
  cases i
  case zero =>
    simp only [shift]
    simp only [Var.openList]
    simp
  case succ i =>
    simp only [shift]
    simp only [← ih]
    simp
    simp only [Var.openList]
    simp
    split
    case _ c1 =>
      have s1 : i < tl.length
      linarith
      simp only [s1]
      simp
    case _ c1 =>
      have s1 : ¬ i < tl.length
      linarith
      simp only [s1]
      simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (free_ x)
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = shiftList D V (List.map (V ∘ free_) tl) (free_ x)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = shiftList D V (List.map (V ∘ free_) tl) (free_ x)
Tactic:
simp only [← ih]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (free_ x)) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = (V ∘ Var.openList 0 (List.map free_ tl)) (free_ x)
Tactic:
simp
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
x : String
⊢ V (free_ x) = V (Var.openList 0 (List.map free_ tl) (free_ x))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ i)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ i)
Tactic:
cases i
Proof state after:
case zero
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)

case succ
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
n✝ : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (n✝ + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (n✝ + 1))
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)
Tactic:
case zero =>
  simp only [shift]
  simp only [Var.openList]
  simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
i : ℕ
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ (i + 1))) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ (i + 1))
Tactic:
case succ i =>
  simp only [shift]
  simp only [← ih]
  simp
  simp only [Var.openList]
  simp
  split
  case _ c1 =>
    have s1 : i < tl.length
    linarith
    simp only [s1]
    simp
  case _ c1 =>
    have s1 : ¬ i < tl.length
    linarith
    simp only [s1]
    simp
Proof state after:
no goals
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) =
    shift D (shiftList D V (List.map (V ∘ free_) tl)) (V (free_ hd)) (bound_ 0)
Tactic:
simp only [shift]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) = V (free_ hd)
Theorem: LN.ShiftListVarOpenList
Proof state before:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V (Var.openList 0 (free_ hd :: List.map free_ tl) (bound_ 0)) = V (free_ hd)
Tactic:
simp only [Var.openList]
Proof state after:
D : Type
V : VarAssignment D
hd : String
tl : List String
ih : V ∘ Var.openList 0 (List.map free_ tl) = shiftList D V (List.map (V ∘ free_) tl)
⊢ V
      (if 0 < 0 then bound_ 0
      else
        if x : 0 - 0 < (free_ hd :: List.map free_ tl).length then (free_ hd :: List.map free_ tl)[0 - 0]
        else bound_ (0 - 0 - (free_ hd :: List.map free_ tl).length + 0)) =
    V (free_ hd)