internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ I.pred_var_ (τ X) [] ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)
Tactic:
simp only [if_pos c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)
Tactic:
simp only [if_neg c1]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (eq_ x y)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (eq_ x y) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (eq_ x y) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ false_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) false_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) false_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds] at phi_ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [sub]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi).not_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi).not_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ¬Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ¬Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi
Tactic:
apply phi_ih
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [Holds] at phi_ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [Holds] at psi_ih
Proof state after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)