internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ (phi.iff_ psi) = phi.iff_ psi
Tactic:
simp only [sub]
Proof state after:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (sub τ phi).iff_ (sub τ psi) = phi.iff_ psi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ (sub τ phi).iff_ (sub τ psi) = phi.iff_ psi
Tactic:
congr!
Proof state after:
case h.e'_1
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ phi = phi

case h.e'_2
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ psi = psi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
case h.e'_1
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ phi = phi
Tactic:
exact phi_ih h1_left
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
case h.e'_2
τ : PredName → PredName
phi psi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
psi_ih : psi.predVarSet = ∅ → sub τ psi = psi
h1_left : phi.predVarSet = ∅
h1_right : psi.predVarSet = ∅
⊢ sub τ psi = psi
Tactic:
exact psi_ih h1_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : (exists_ x phi).predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Tactic:
simp only [predVarSet] at h1
Proof state after:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ (exists_ x phi) = exists_ x phi
Tactic:
simp only [sub]
Proof state after:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (sub τ phi) = exists_ x phi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ exists_ x (sub τ phi) = exists_ x phi
Tactic:
congr!
Proof state after:
case h.e'_2
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
case h.e'_2
τ : PredName → PredName
x : VarName
phi : Formula
phi_ih : phi.predVarSet = ∅ → sub τ phi = phi
h1 : phi.predVarSet = ∅
⊢ sub τ phi = phi
Tactic:
exact phi_ih h1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.sub_no_predVar
Proof state before:
τ : PredName → PredName
X : DefName
xs : List VarName
h1 : (def_ X xs).predVarSet = ∅
⊢ sub τ (def_ X xs) = def_ X xs
Tactic:
simp only [sub]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → PredName
F : Formula
⊢ Holds D I V E (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V E (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V E F
Tactic:
induction E generalizing F V
Proof state after:
case nil
D : Type
I : Interpretation D
τ : PredName → PredName
V : VarAssignment D
F : Formula
⊢ Holds D I V [] (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] F

case cons
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
F : Formula
⊢ Holds D I V (head✝ :: tail✝) (sub τ F) ↔
    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✝) F
Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
case nil.def_ X xs =>
  simp only [sub]
  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
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tl (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tl F
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
case cons.def_ hd tl ih X xs =>
  simp only [Holds] at ih
  simp at ih
  simp only [sub]
  simp only [Holds]
  split_ifs
  case _ c1 =>
    specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
    simp only [sub_no_predVar hd.q τ hd.h2] at ih
    apply ih
  case _ c1 =>
    specialize ih V (def_ X xs)
    simp only [sub] at ih
    exact 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
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ 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_const_ X xs)
Tactic:
case pred_const_ X xs =>
  simp only [sub]
  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
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (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:
case pred_var_ X xs =>
    simp only [sub]
    split_ifs
    case pos c1 =>
      simp only [Holds]
      simp
      simp only [if_pos c1]
    case neg c1 =>
      simp only [Holds]
      simp
      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:
case eq_ x y =>
  simp only [sub]
  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:
case true_ | false_ =>
  simp only [sub]
  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:
case not_ phi phi_ih =>
  simp only [Holds] at phi_ih
  simp only [sub]
  simp only [Holds]
  congr! 1
  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
x : VarName
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 τ (exists_ x 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✝) (exists_ x phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [Holds] at phi_ih
  simp only [sub]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intros d
  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
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ 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_const_ X xs)
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 : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ 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_const_ X 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
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ 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_const_ X xs)
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
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (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 [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 : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (if xs = [] then pred_var_ (τ X) [] else 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)
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
⊢ Holds D I V (head✝ :: tail✝) (if xs = [] then pred_var_ (τ X) [] else 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:
split_ifs
Proof state after:
case pos
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
h✝ : xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ (τ X) []) ↔
    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)

case neg
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
h✝ : ¬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)
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) []) ↔
    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:
case pos c1 =>
  simp only [Holds]
  simp
  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:
case neg c1 =>
  simp only [Holds]
  simp
  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 : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ (τ X) []) ↔
    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 []) ↔
    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 []) ↔
    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) [] ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)