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
⊢ (if h : (τ X (List.map V xs).length).isSome = true then
      if (List.map V xs).length = ((τ X (List.map V xs).length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X (List.map V xs).length).get ⋯).1 (List.map V xs)) E
          ((τ X (List.map V xs).length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
Tactic:
simp
Proof state after:
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
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
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
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
Tactic:
split_ifs
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
h✝¹ : (τ X xs.length).isSome = true
h✝ : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

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
h✝¹ : (τ X xs.length).isSome = true
h✝ : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)

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
h✝ : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
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
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
case _ c1 c2 =>
  simp only [Holds]
Proof state after:
no goals
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
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
case _ c1 =>
  simp only [Holds]
Proof state after:
no goals
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let opt := τ X xs.length
Proof state after:
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let val := Option.get opt c1
Proof state after:
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let zs := val.fst
Proof state after:
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let H := val.snd
Proof state after:
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
obtain s1 := Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateListITE id zs xs) c H
Proof state after:
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 (V ∘ Function.updateListITE id zs 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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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 (V ∘ Function.updateListITE id zs 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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp only [Function.updateListITE_comp] at s1
Proof state after:
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 ∘ id) 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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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 ∘ id) 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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp at s1
Proof state after:
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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
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 V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp only [s1]
Proof state after:
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