internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : X' = hd.name ∧ (List.map σ' xs').length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q
Tactic:
simp at c2
Proof state after:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : X' = hd.name ∧ xs'.length = hd.args.length
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' (List.map σ' xs'))) tl hd.q
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ' : VarName → VarName
binders' : Finset VarName
X' : DefName
xs' : List VarName
ih_1 : ∀ v ∈ xs', v ∉ binders' → σ' v ∉ binders'
V V' : VarAssignment D
h2 : ∀ v ∈ binders', V v = V' (σ' v)
h3 : ∀ (v : VarName), σ' v ∉ binders' → V v = V' (σ' v)
h4 : ∀ v ∈ binders', v = σ' v
hd : Definition
tl : List Definition
ih : Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
c1 : ¬(X' = hd.name ∧ xs'.length = hd.args.length)
c2 : ¬(X' = hd.name ∧ (List.map σ' xs').length = hd.args.length)
⊢ Holds D I V tl (def_ X' xs') ↔ Holds D I V' tl (def_ X' (List.map σ' xs'))
Tactic:
exact ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ Holds D I (V ∘ σ) E F ↔ Holds D I V E F'
Tactic:
apply substitution_theorem_aux D I (V ∘ σ) V E σ ∅ F F' h1
Proof state after:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ v ∈ ∅, (V ∘ σ) v = V (σ v)

case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ (v : VarName), σ v ∉ ∅ → (V ∘ σ) v = V (σ v)

case h4
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ v ∈ ∅, v = σ v
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem
Proof state before:
case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ v ∈ ∅, (V ∘ σ) v = V (σ v)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem
Proof state before:
case h3
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ (v : VarName), σ v ∉ ∅ → (V ∘ σ) v = V (σ v)
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem
Proof state before:
case h4
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
⊢ ∀ v ∈ ∅, v = σ v
Tactic:
simp
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_is_valid
Proof state before:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : F.IsValid
⊢ F'.IsValid
Tactic:
simp only [IsValid] at h2
Proof state after:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ F'.IsValid
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_is_valid
Proof state before:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ F'.IsValid
Tactic:
simp only [IsValid]
Proof state after:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_is_valid
Proof state before:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
⊢ ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F'
Tactic:
intro D I V E
Proof state after:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E F'
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_is_valid
Proof state before:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I V E F'
Tactic:
simp only [← substitution_theorem D I V E σ F F' h1]
Proof state after:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Theorem: FOL.NV.Sub.Var.All.Ind.substitution_is_valid
Proof state before:
σ : VarName → VarName
F F' : Formula
h1 : IsSub σ F F'
h2 : ∀ (D : Type) (I : Interpretation D) (V : VarAssignment D) (E : Env), Holds D I V E F
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
⊢ Holds D I (V ∘ σ) E F
Tactic:
apply h2
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
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace c τ (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  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 y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace c τ (eq_ x y))
Tactic:
case eq_ x y =>
  simp only [replace]
  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)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace c τ false_)
Tactic:
case true_ | false_ =>
  simp only [replace]
  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)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi.not_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  congr! 1
  exact phi_ih V binders h1 h2
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 : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ x phi)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace c τ (exists_ x phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  intro v a1
  simp only [Function.updateITE]
  simp at a1
  push_neg at a1
  cases a1
  case h.intro a1_left a1_right =>
    simp only [if_neg a1_right]
    exact h2 v a1_left
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
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace c τ (pred_const_ X xs))
Tactic:
simp only [replace]
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
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ 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
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)
Tactic:
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
h1 : admitsAux τ binders (pred_var_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
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
    if xs.length = ((τ X xs.length).get ⋯).1.length then
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
    else True
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (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
    if xs.length = ((τ X xs.length).get ⋯).1.length then
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
    else True
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp at h1
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
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (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
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp only [replace]
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
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X 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
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X 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 only [Holds]
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 (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)