internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
Tactic:
apply Holds_coincide_Var
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ ∀ (v : VarName),
    isFreeIn v ((τ X xs.length).get ⋯).2 →
      Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v =
        Function.updateListITE V zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ ∀ (v : VarName),
    isFreeIn v ((τ X xs.length).get ⋯).2 →
      Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v =
        Function.updateListITE V zs (List.map V xs) v
Tactic:
intro v a1
Proof state after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
by_cases c3 : v ∈ zs
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
apply Function.updateListITE_mem_eq_len V' V v zs (List.map V xs) c3
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Tactic:
simp
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = xs.length
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = xs.length
Tactic:
simp only [← c2]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
simp only [Function.updateListITE_not_mem V v zs (List.map V xs) c3]
Proof state after:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = V v
Tactic:
simp only [Function.updateListITE_not_mem V' v zs (List.map V xs) c3]
Proof state after:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ V' v = V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ V' v = V v
Tactic:
apply h2
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ v ∉ binders
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ v ∉ binders
Tactic:
intro contra
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
contra : v ∈ binders
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
contra : v ∈ binders
⊢ False
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
⊢ False