Theorem: FOL.NV.replace_empty_Holds
Proof state before:
case cons
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
V : VarAssignment D
F : Formula
h1 : ¬isFreeIn v F
h2 : ¬isBoundIn v F
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) F ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v F)
Tactic:
induction F generalizing V
Proof state after:
case cons.pred_const_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (pred_const_ a✝¹ a✝)
h2 : ¬isBoundIn v (pred_const_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_const_ a✝¹ a✝))

case cons.pred_var_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (pred_var_ a✝¹ a✝)
h2 : ¬isBoundIn v (pred_var_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_var_ a✝¹ a✝))

case cons.eq_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ a✝ : VarName
V : VarAssignment D
h1 : ¬isFreeIn v (eq_ a✝¹ a✝)
h2 : ¬isBoundIn v (eq_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (eq_ a✝¹ a✝))

case cons.true_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
V : VarAssignment D
h1 : ¬isFreeIn v true_
h2 : ¬isBoundIn v true_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) true_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v true_)

case cons.false_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
V : VarAssignment D
h1 : ¬isFreeIn v false_
h2 : ¬isBoundIn v false_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) false_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v false_)

case cons.not_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v a✝.not_
h2 : ¬isBoundIn v a✝.not_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝.not_)

case cons.imp_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝¹ →
      ¬isBoundIn v a✝¹ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝¹ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (a✝¹.imp_ a✝)
h2 : ¬isBoundIn v (a✝¹.imp_ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (a✝¹.imp_ a✝))

case cons.and_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝¹ →
      ¬isBoundIn v a✝¹ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝¹ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (a✝¹.and_ a✝)
h2 : ¬isBoundIn v (a✝¹.and_ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (a✝¹.and_ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (a✝¹.and_ a✝))

case cons.or_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝¹ →
      ¬isBoundIn v a✝¹ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝¹ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (a✝¹.or_ a✝)
h2 : ¬isBoundIn v (a✝¹.or_ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (a✝¹.or_ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (a✝¹.or_ a✝))

case cons.iff_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝¹ →
      ¬isBoundIn v a✝¹ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝¹ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (a✝¹.iff_ a✝)
h2 : ¬isBoundIn v (a✝¹.iff_ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (a✝¹.iff_ a✝))

case cons.forall_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (forall_ a✝¹ a✝)
h2 : ¬isBoundIn v (forall_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (forall_ a✝¹ a✝))

case cons.exists_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v a✝ →
      ¬isBoundIn v a✝ →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) a✝ ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v a✝))
V : VarAssignment D
h1 : ¬isFreeIn v (exists_ a✝¹ a✝)
h2 : ¬isBoundIn v (exists_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ a✝¹ a✝))

case cons.def_
D : Type
I : Interpretation D
u v : VarName
a : D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V v a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u v F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ a✝¹ a✝)
h2 : ¬isBoundIn v (def_ a✝¹ a✝)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (def_ a✝¹ a✝))