internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
exact s1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
h✝ : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
case pos c2 =>
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)
Tactic:
case neg c2 =>
  simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (replace P zs H (eq_ x y))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (eq_ x y)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref (replace P zs H false_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref false_
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi).not_
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi).not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ¬Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ ¬Holds D I V E_ref (replace P zs H phi)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ¬Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ ¬Holds D I V E_ref (replace P zs H phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)
Tactic:
exact phi_ih V binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (phi.iff_ psi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔ Holds D I V E_ref (replace P zs H (phi.iff_ psi))
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔ Holds D I V E_ref (replace P zs H (phi.iff_ psi))