Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem
Proof state before:
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
Tactic:
induction F generalizing V
Proof state after:
case cons.pred_const_
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
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ a✝¹ a✝)) ↔
    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_ a✝¹ a✝)

case cons.pred_var_
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
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_var_ a✝¹ a✝)) ↔
    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_ a✝¹ a✝)

case cons.eq_
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
a✝¹ a✝ : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (eq_ a✝¹ a✝)) ↔
    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_ a✝¹ a✝)

case cons.true_
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 τ true_) ↔
    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✝) true_

case cons.false_
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_

case cons.not_
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
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ a✝.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✝) a✝.not_

case cons.imp_
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
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      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✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.imp_ a✝)) ↔
    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✝) (a✝¹.imp_ a✝)

case cons.and_
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
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      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✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.and_ a✝)) ↔
    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✝) (a✝¹.and_ a✝)

case cons.or_
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
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      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✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.or_ a✝)) ↔
    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✝) (a✝¹.or_ a✝)

case cons.iff_
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
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      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✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.iff_ a✝)) ↔
    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✝) (a✝¹.iff_ a✝)

case cons.forall_
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
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (forall_ a✝¹ a✝)) ↔
    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✝) (forall_ a✝¹ a✝)

case cons.exists_
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
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      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✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ a✝¹ a✝)) ↔
    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_ a✝¹ a✝)

case cons.def_
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
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (def_ a✝¹ a✝)) ↔
    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✝) (def_ a✝¹ a✝)