Theorem: FOL.NV.replace_empty_Holds (FOL/NV/Alpha.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
u v : VarName
F : Formula
a : D
h1 : ¬isFreeIn v F
h2 : ¬isBoundIn v F
⊢ Holds D I (Function.updateITE V u a) E F ↔
    Holds D I (Function.updateITE V v a) E (Sub.Var.One.Rec.fastReplaceFree u v F)
Tactic:
induction E generalizing F V
State after:
case nil
D : Type
I : Interpretation D
u v : VarName
a : D
V : VarAssignment D
F : Formula
h1 : ¬isFreeIn v F
h2 : ¬isBoundIn v F
⊢ Holds D I (Function.updateITE V u a) [] F ↔
    Holds D I (Function.updateITE V v a) [] (Sub.Var.One.Rec.fastReplaceFree u v F)

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)

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (Sub.Var.One.Rec.fastReplaceFree u v (def_ X xs))
Tactic:
case nil.def_ X xs =>
  simp only [Sub.Var.One.Rec.fastReplaceFree]
  simp only [Holds]
State after:
no goals

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
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✝))

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (pred_var_ X xs)
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_var_ X xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  simp only [isFreeIn] at h1
  simp only [Sub.Var.One.Rec.fastReplaceFree]
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  simp only [Function.updateITE]
  simp only [eq_comm]
  split_ifs
  case _ c1 c2 =>
    rfl
  case _ c1 c2 =>
    contradiction
  case _ c1 c2 =>
    subst c2
    contradiction
  case _ c1 c2 =>
    rfl
State after:
no goals

State before:
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_)
Tactic:
case true_ | false_ =>
  simp only [Sub.Var.One.Rec.fastReplaceFree]
  simp only [Holds]
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi.not_
h2 : ¬isBoundIn v phi.not_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [isFreeIn] at h1
  simp only [isBoundIn] at h2
  simp only [Sub.Var.One.Rec.fastReplaceFree]
  simp only [Holds]
  congr! 1
  exact phi_ih V h1 h2
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (pred_var_ X xs)
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_var_ X xs))
Tactic:
simp only [isFreeIn] at h1
State after:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_var_ X xs))

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (pred_var_ X xs))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (pred_var_ X (List.map (fun x => if u = x then v else x) xs))

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (pred_var_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
simp only [Holds]
State after:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ I.pred_var_ X (List.map (Function.updateITE V u a) xs) ↔
    I.pred_var_ X (List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs))

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ I.pred_var_ X (List.map (Function.updateITE V u a) xs) ↔
    I.pred_var_ X (List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs))
Tactic:
congr! 1
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ List.map (Function.updateITE V u a) xs =
    List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs)

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ List.map (Function.updateITE V u a) xs =
    List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs)
Tactic:
simp
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ List.map (Function.updateITE V u a) xs = List.map (Function.updateITE V v a ∘ fun x => if u = x then v else x) xs

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ List.map (Function.updateITE V u a) xs = List.map (Function.updateITE V v a ∘ fun x => if u = x then v else x) xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ ∀ x ∈ xs, Function.updateITE V u a x = (Function.updateITE V v a ∘ fun x => if u = x then v else x) x

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
⊢ ∀ x ∈ xs, Function.updateITE V u a x = (Function.updateITE V v a ∘ fun x => if u = x then v else x) x
Tactic:
intro x a1
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V u a x = (Function.updateITE V v a ∘ fun x => if u = x then v else x) x

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V u a x = (Function.updateITE V v a ∘ fun x => if u = x then v else x) x
Tactic:
simp
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V u a x = Function.updateITE V v a (if u = x then v else x)

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V u a x = Function.updateITE V v a (if u = x then v else x)
Tactic:
simp only [Function.updateITE]
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ (if x = u then a else V x) = if (if u = x then v else x) = v then a else V (if u = x then v else x)

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ (if x = u then a else V x) = if (if u = x then v else x) = v then a else V (if u = x then v else x)
Tactic:
simp only [eq_comm]
State after:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ (if u = x then a else V x) = if v = if u = x then v else x then a else V (if u = x then v else x)

State before:
case a.h.e'_4
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
⊢ (if u = x then a else V x) = if v = if u = x then v else x then a else V (if u = x then v else x)
Tactic:
split_ifs
State after:
case pos
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
h✝¹ : u = x
h✝ : v = v
⊢ a = a

case neg
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
h✝¹ : u = x
h✝ : ¬v = v
⊢ a = V v

case pos
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
h✝¹ : ¬u = x
h✝ : v = x
⊢ V x = a

case neg
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
h✝¹ : ¬u = x
h✝ : ¬v = x
⊢ V x = V x

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : u = x
c2 : v = v
⊢ a = a
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : u = x
c2 : ¬v = v
⊢ a = V v
Tactic:
case _ c1 c2 =>
  contradiction
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : ¬u = x
c2 : v = x
⊢ V x = a
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : ¬u = x
c2 : ¬v = x
⊢ V x = V x
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : u = x
c2 : v = v
⊢ a = a
Tactic:
rfl
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : u = x
c2 : ¬v = v
⊢ a = V v
Tactic:
contradiction
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : ¬u = x
c2 : v = x
⊢ V x = a
Tactic:
subst c2
State after:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
a1 : v ∈ xs
c1 : ¬u = v
⊢ V v = a

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
a1 : v ∈ xs
c1 : ¬u = v
⊢ V v = a
Tactic:
contradiction
State after:
no goals

State before:
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))
X : PredName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (pred_var_ X xs)
x : VarName
a1 : x ∈ xs
c1 : ¬u = x
c2 : ¬v = x
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
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))
x y : VarName
V : VarAssignment D
h1 : ¬isFreeIn v (eq_ x y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ x y) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (eq_ x y))
Tactic:
simp only [isFreeIn] at h1
State after:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ x y) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (eq_ x y))

State before:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ x y) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (eq_ x y))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ x y) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (eq_ (if u = x then v else x) (if u = y then v else y))

State before:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (eq_ x y) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (eq_ (if u = x then v else x) (if u = y then v else y))
Tactic:
simp only [Holds]
State after:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a x = Function.updateITE V u a y ↔
    Function.updateITE V v a (if u = x then v else x) = Function.updateITE V v a (if u = y then v else y)

State before:
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a x = Function.updateITE V u a y ↔
    Function.updateITE V v a (if u = x then v else x) = Function.updateITE V v a (if u = y then v else y)
Tactic:
congr! 1
State after:
case a.h.e'_2
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a x = Function.updateITE V v a (if u = x then v else x)

case a.h.e'_3
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a y = Function.updateITE V v a (if u = y then v else y)

State before:
case a.h.e'_2
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a x = Function.updateITE V v a (if u = x then v else x)
Tactic:
simp only [Function.updateITE]
State after:
case a.h.e'_2
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ (if x = u then a else V x) = if (if u = x then v else x) = v then a else V (if u = x then v else x)

State before:
case a.h.e'_2
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ (if x = u then a else V x) = if (if u = x then v else x) = v then a else V (if u = x then v else x)
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
case a.h.e'_3
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ Function.updateITE V u a y = Function.updateITE V v a (if u = y then v else y)
Tactic:
simp only [Function.updateITE]
State after:
case a.h.e'_3
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ (if y = u then a else V y) = if (if u = y then v else y) = v then a else V (if u = y then v else y)

State before:
case a.h.e'_3
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))
x y : VarName
V : VarAssignment D
h1 : ¬(v = x ∨ v = y)
h2 : ¬isBoundIn v (eq_ x y)
⊢ (if y = u then a else V y) = if (if u = y then v else y) = v then a else V (if u = y then v else y)
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
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_)
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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✝) false_

State before:
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✝) false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi.not_
h2 : ¬isBoundIn v phi.not_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)
Tactic:
simp only [isFreeIn] at h1
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi.not_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi.not_
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)
Tactic:
simp only [isBoundIn] at h2
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi.not_)
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi).not_

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi.not_ ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi).not_
Tactic:
simp only [Holds]
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ ¬Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    ¬Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ ¬Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    ¬Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case a.h.e'_1.a
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v phi
h2 : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
exact phi_ih V h1 h2
State after:
no goals

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1 : ¬isFreeIn v (phi.iff_ psi)
h2 : ¬isBoundIn v (phi.iff_ psi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
simp only [isFreeIn] at h1
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1 : ¬(isFreeIn v phi ∨ isFreeIn v psi)
h2 : ¬isBoundIn v (phi.iff_ psi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1 : ¬(isFreeIn v phi ∨ isFreeIn v psi)
h2 : ¬isBoundIn v (phi.iff_ psi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
push_neg at h1
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬isBoundIn v (phi.iff_ psi)
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬isBoundIn v (phi.iff_ psi)
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
simp only [isBoundIn] at h2
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬(isBoundIn v phi ∨ isBoundIn v psi)
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬(isBoundIn v phi ∨ isBoundIn v psi)
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
push_neg at h2
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
h2 : ¬isBoundIn v phi ∧ ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1 : ¬isFreeIn v phi ∧ ¬isFreeIn v psi
h2 : ¬isBoundIn v phi ∧ ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
cases h1
State after:
case intro
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬isBoundIn v phi ∧ ¬isBoundIn v psi
left✝ : ¬isFreeIn v phi
right✝ : ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h2 : ¬isBoundIn v phi ∧ ¬isBoundIn v psi
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
cases h2
State after:
case intro
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
left✝ : ¬isBoundIn v phi
right✝ : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (phi.iff_ psi))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝)
      ((Sub.Var.One.Rec.fastReplaceFree u v phi).iff_ (Sub.Var.One.Rec.fastReplaceFree u v psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (phi.iff_ psi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝)
      ((Sub.Var.One.Rec.fastReplaceFree u v phi).iff_ (Sub.Var.One.Rec.fastReplaceFree u v psi))
Tactic:
simp only [Holds]
State after:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi) ↔
    (Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi) ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))

State before:
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi) ↔
    (Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi) ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
Tactic:
congr! 1
State after:
case a.h.e'_1.a
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)

case a.h.e'_2.a
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi)

State before:
case a.h.e'_1.a
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
exact phi_ih V h1_left h2_left
State after:
no goals

State before:
case a.h.e'_2.a
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))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
psi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v psi →
      ¬isBoundIn v psi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi))
V : VarAssignment D
h1_left : ¬isFreeIn v phi
h1_right : ¬isFreeIn v psi
h2_left : ¬isBoundIn v phi
h2_right : ¬isBoundIn v psi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) psi ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v psi)
Tactic:
exact psi_ih V h1_right h2_right
State after:
no goals

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬isFreeIn v (exists_ x phi)
h2 : ¬isBoundIn v (exists_ x phi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
simp only [isFreeIn] at h1
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬(¬v = x ∧ isFreeIn v phi)
h2 : ¬isBoundIn v (exists_ x phi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : ¬(¬v = x ∧ isFreeIn v phi)
h2 : ¬isBoundIn v (exists_ x phi)
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
push_neg at h1
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2 : ¬isBoundIn v (exists_ x phi)
h1 : v ≠ x → ¬isFreeIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2 : ¬isBoundIn v (exists_ x phi)
h1 : v ≠ x → ¬isFreeIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
simp only [isBoundIn] at h2
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2 : ¬(v = x ∨ isBoundIn v phi)
h1 : v ≠ x → ¬isFreeIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2 : ¬(v = x ∨ isBoundIn v phi)
h1 : v ≠ x → ¬isFreeIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
push_neg at h2
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2 : v ≠ x ∧ ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2 : v ≠ x ∧ ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
cases h2
State after:
case intro
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
left✝ : v ≠ x
right✝ : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v (exists_ x phi))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝)
      (if u = x then exists_ x phi else exists_ x (Sub.Var.One.Rec.fastReplaceFree u v phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝)
      (if u = x then exists_ x phi else exists_ x (Sub.Var.One.Rec.fastReplaceFree u v phi))
Tactic:
split_ifs
State after:
case pos
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
h✝ : u = x
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ x phi)

case neg
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
h✝ : ¬u = x
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ x (Sub.Var.One.Rec.fastReplaceFree u v phi))

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : u = x
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ x phi)
Tactic:
case pos c1 =>
  subst c1
  apply Holds_coincide_Var
  intro x a1
  simp only [isFreeIn] at a1
  cases a1
  case h1.intro a1_left a1_right =>
    simp only [Function.updateITE]
    simp only [if_neg a1_left]
    split_ifs
    case pos c2 =>
      subst c2
      tauto
    case neg c2 =>
      rfl
State after:
no goals

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : u = x
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ x phi)
Tactic:
subst c1
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ u phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ u phi)

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ u phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ u phi)
Tactic:
apply Holds_coincide_Var
State after:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
⊢ ∀ (v_1 : VarName), isFreeIn v_1 (exists_ u phi) → Function.updateITE V u a v_1 = Function.updateITE V v a v_1

State before:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
⊢ ∀ (v_1 : VarName), isFreeIn v_1 (exists_ u phi) → Function.updateITE V u a v_1 = Function.updateITE V v a v_1
Tactic:
intro x a1
State after:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1 : isFreeIn x (exists_ u phi)
⊢ Function.updateITE V u a x = Function.updateITE V v a x

State before:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1 : isFreeIn x (exists_ u phi)
⊢ Function.updateITE V u a x = Function.updateITE V v a x
Tactic:
simp only [isFreeIn] at a1
State after:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1 : ¬x = u ∧ isFreeIn x phi
⊢ Function.updateITE V u a x = Function.updateITE V v a x

State before:
case h1
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1 : ¬x = u ∧ isFreeIn x phi
⊢ Function.updateITE V u a x = Function.updateITE V v a x
Tactic:
cases a1
State after:
case h1.intro
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
left✝ : ¬x = u
right✝ : isFreeIn x phi
⊢ Function.updateITE V u a x = Function.updateITE V v a x

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ Function.updateITE V u a x = Function.updateITE V v a x
Tactic:
case h1.intro a1_left a1_right =>
  simp only [Function.updateITE]
  simp only [if_neg a1_left]
  split_ifs
  case pos c2 =>
    subst c2
    tauto
  case neg c2 =>
    rfl
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ Function.updateITE V u a x = Function.updateITE V v a x
Tactic:
simp only [Function.updateITE]
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ (if x = u then a else V x) = if x = v then a else V x

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ (if x = u then a else V x) = if x = v then a else V x
Tactic:
simp only [if_neg a1_left]
State after:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ V x = if x = v then a else V x

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
⊢ V x = if x = v then a else V x
Tactic:
split_ifs
State after:
case pos
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
h✝ : x = v
⊢ V x = a

case neg
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
h✝ : ¬x = v
⊢ V x = V x

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
c2 : x = v
⊢ V x = a
Tactic:
case pos c2 =>
  subst c2
  tauto
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
c2 : ¬x = v
⊢ V x = V x
Tactic:
case neg c2 =>
  rfl
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
c2 : x = v
⊢ V x = a
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
u : VarName
a : D
head✝ : Definition
tail✝ : List Definition
phi : Formula
V : VarAssignment D
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn x F →
      ¬isBoundIn x F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V x a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u x F))
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn x phi →
      ¬isBoundIn x phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u x phi))
h2_right : ¬isBoundIn x phi
h1 : x ≠ u → ¬isFreeIn x phi
h2_left : x ≠ u
⊢ V x = a

State before:
D : Type
I : Interpretation D
u : VarName
a : D
head✝ : Definition
tail✝ : List Definition
phi : Formula
V : VarAssignment D
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn x F →
      ¬isBoundIn x F →
        (Holds D I (Function.updateITE V u a) tail✝ F ↔
          Holds D I (Function.updateITE V x a) tail✝ (Sub.Var.One.Rec.fastReplaceFree u x F))
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn x phi →
      ¬isBoundIn x phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u x phi))
h2_right : ¬isBoundIn x phi
h1 : x ≠ u → ¬isFreeIn x phi
h2_left : x ≠ u
⊢ V x = a
Tactic:
tauto
State after:
no goals

State before:
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))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h2_right : ¬isBoundIn v phi
h1 : v ≠ u → ¬isFreeIn v phi
h2_left : v ≠ u
x : VarName
a1_left : ¬x = u
a1_right : isFreeIn x phi
c2 : ¬x = v
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ Holds D I (Function.updateITE V u a) (head✝ :: tail✝) (exists_ x phi) ↔
    Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (exists_ x (Sub.Var.One.Rec.fastReplaceFree u v phi))
Tactic:
simp only [Holds]
State after:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi) ↔
    ∃ d,
      Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi) ↔
    ∃ d,
      Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ ∀ (a_1 : D),
    Holds D I (Function.updateITE (Function.updateITE V u a) x a_1) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE (Function.updateITE V v a) x a_1) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ ∀ (a_1 : D),
    Holds D I (Function.updateITE (Function.updateITE V u a) x a_1) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE (Function.updateITE V v a) x a_1) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
intro d
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
simp only [Function.updateITE_comm V v x d a h2_left]
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V x d) v a) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V x d) v a) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
simp only [Function.updateITE_comm V u x d a c1]
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V x d) v a) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) u a) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V x d) v a) (head✝ :: tail✝)
      (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
apply phi_ih
State after:
case h.h1
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ ¬isFreeIn v phi

case h.h2
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ ¬isBoundIn v phi

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D),
      Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
apply forall_congr'
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ ∀ (a_1 : D),
    Holds D I (Function.updateITE (Function.updateITE V u a) x a_1) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE (Function.updateITE V v a) x a_1) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V u a) x d) (head✝ :: tail✝) phi) ↔
    ∃ d,
      Holds D I (Function.updateITE (Function.updateITE V v a) x d) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)
Tactic:
apply exists_congr
State after:
case h
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
⊢ ∀ (a_1 : D),
    Holds D I (Function.updateITE (Function.updateITE V u a) x a_1) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE (Function.updateITE V v a) x a_1) (head✝ :: tail✝)
        (Sub.Var.One.Rec.fastReplaceFree u v phi)

State before:
case h.h1
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ ¬isFreeIn v phi
Tactic:
exact h1 h2_left
State after:
no goals

State before:
case h.h2
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))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    ¬isFreeIn v phi →
      ¬isBoundIn v phi →
        (Holds D I (Function.updateITE V u a) (head✝ :: tail✝) phi ↔
          Holds D I (Function.updateITE V v a) (head✝ :: tail✝) (Sub.Var.One.Rec.fastReplaceFree u v phi))
V : VarAssignment D
h1 : v ≠ x → ¬isFreeIn v phi
h2_left : v ≠ x
h2_right : ¬isBoundIn v phi
c1 : ¬u = x
d : D
⊢ ¬isBoundIn v phi
Tactic:
exact h2_right
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (Sub.Var.One.Rec.fastReplaceFree u v (def_ X xs))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (def_ X (List.map (fun x => if u = x then v else x) xs))

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) (hd :: tl) (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) (hd :: tl) (Sub.Var.One.Rec.fastReplaceFree u v (def_ X xs))
Tactic:
simp only [Sub.Var.One.Rec.fastReplaceFree]
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) (hd :: tl) (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) (hd :: tl) (def_ X (List.map (fun x => if u = x then v else x) xs))

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) (hd :: tl) (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) (hd :: tl) (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V u a) hd.args (List.map (Function.updateITE V u a) xs)) tl
        hd.q
    else Holds D I (Function.updateITE V u a) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v a) hd.args
          (List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs)))
        tl hd.q
    else Holds D I (Function.updateITE V v a) tl (def_ X (List.map (fun x => if u = x then v else x) xs))

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE (Function.updateITE V u a) hd.args (List.map (Function.updateITE V u a) xs)) tl
        hd.q
    else Holds D I (Function.updateITE V u a) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v a) hd.args
          (List.map (Function.updateITE V v a) (List.map (fun x => if u = x then v else x) xs)))
        tl hd.q
    else Holds D I (Function.updateITE V v a) tl (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
unfold Function.updateITE
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (fun c => if c = u then a else V c) hd.args
          (List.map (fun c => if c = u then a else V c) xs))
        tl hd.q
    else Holds D I (fun c => if c = u then a else V c) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length then
      Holds D I
        (Function.updateListITE (fun c => if c = v then a else V c) hd.args
          (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
        tl hd.q
    else Holds D I (fun c => if c = v then a else V c) tl (def_ X (List.map (fun x => if u = x then v else x) xs))

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (fun c => if c = u then a else V c) hd.args
          (List.map (fun c => if c = u then a else V c) xs))
        tl hd.q
    else Holds D I (fun c => if c = u then a else V c) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length then
      Holds D I
        (Function.updateListITE (fun c => if c = v then a else V c) hd.args
          (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
        tl hd.q
    else Holds D I (fun c => if c = v then a else V c) tl (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
congr! 1
State after:
case a.h₁.a
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ X = hd.name ∧ xs.length = hd.args.length ↔
    X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length

case a.h₂.a
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = u then a else V c) hd.args
        (List.map (fun c => if c = u then a else V c) xs))
      tl hd.q ↔
    Holds D I
      (Function.updateListITE (fun c => if c = v then a else V c) hd.args
        (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
      tl hd.q

case a.h₃.a
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ Holds D I (fun c => if c = u then a else V c) tl (def_ X xs) ↔
    Holds D I (fun c => if c = v then a else V c) tl (def_ X (List.map (fun x => if u = x then v else x) xs))

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ X = hd.name ∧ xs.length = hd.args.length ↔
    X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
Tactic:
case _ =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ X = hd.name ∧ xs.length = hd.args.length ↔
    X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = u then a else V c) hd.args
        (List.map (fun c => if c = u then a else V c) xs))
      tl hd.q ↔
    Holds D I
      (Function.updateListITE (fun c => if c = v then a else V c) hd.args
        (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
      tl hd.q
Tactic:
simp only [isFreeIn] at h1
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = u then a else V c) hd.args
        (List.map (fun c => if c = u then a else V c) xs))
      tl hd.q ↔
    Holds D I
      (Function.updateListITE (fun c => if c = v then a else V c) hd.args
        (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
      tl hd.q

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = u then a else V c) hd.args
        (List.map (fun c => if c = u then a else V c) xs))
      tl hd.q ↔
    Holds D I
      (Function.updateListITE (fun c => if c = v then a else V c) hd.args
        (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)))
      tl hd.q
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ ∀ (v_1 : VarName),
    isFreeIn v_1 hd.q →
      Function.updateListITE (fun c => if c = u then a else V c) hd.args
          (List.map (fun c => if c = u then a else V c) xs) v_1 =
        Function.updateListITE (fun c => if c = v then a else V c) hd.args
          (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)) v_1

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
⊢ ∀ (v_1 : VarName),
    isFreeIn v_1 hd.q →
      Function.updateListITE (fun c => if c = u then a else V c) hd.args
          (List.map (fun c => if c = u then a else V c) xs) v_1 =
        Function.updateListITE (fun c => if c = v then a else V c) hd.args
          (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)) v_1
Tactic:
intro v' a1
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)) v'

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map (fun c => if c = v then a else V c) (List.map (fun x => if u = x then v else x) xs)) v'
Tactic:
simp
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'
Tactic:
have s1 : (List.map ((fun (a_1 : VarName) => if a_1 = v then a else V a_1) ∘ fun (x : VarName) => if u = x then v else x) xs) = (List.map (fun (a_1 : VarName) => if a_1 = u then a else V a_1) xs)
State after:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs

case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs

case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'
Tactic:
{
  simp only [List.map_eq_map_iff]
  intro x a2
  simp only [eq_comm]
  simp
  split_ifs
  case _ =>
    rfl
  case _ =>
    contradiction
  case _ c1 c2 =>
    subst c2
    contradiction
  case _ =>
    rfl
}
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args
      (List.map ((fun c => if c = v then a else V c) ∘ fun x => if u = x then v else x) xs) v'
Tactic:
simp only [s1]
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v'

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ Function.updateListITE (fun c => if c = u then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v' =
    Function.updateListITE (fun c => if c = v then a else V c) hd.args (List.map (fun c => if c = u then a else V c) xs)
      v'
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ v' ∈ hd.args

case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ xs, ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) x = if x = u then a else V x

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ ∀ x ∈ xs, ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) x = if x = u then a else V x
Tactic:
intro x a2
State after:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) x = if x = u then a else V x

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) x = if x = u then a else V x
Tactic:
simp only [eq_comm]
State after:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ (if u = x then a else V x) = ((fun a_1 => if v = a_1 then a else V a_1) ∘ fun x => if u = x then v else x) x

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ (if u = x then a else V x) = ((fun a_1 => if v = a_1 then a else V a_1) ∘ fun x => if u = x then v else x) x
Tactic:
simp
State after:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ (if u = x then a else V x) = if v = if u = x then v else x then a else V (if u = x then v else x)

State before:
case s1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
⊢ (if u = x then a else V x) = if v = if u = x then v else x then a else V (if u = x then v else x)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : v = v
⊢ a = a

case neg
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : ¬v = v
⊢ a = V v

case pos
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : ¬u = x
h✝ : v = x
⊢ V x = a

case neg
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : ¬u = x
h✝ : ¬v = x
⊢ V x = V x

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : v = v
⊢ a = a
Tactic:
case _ =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : ¬v = v
⊢ a = V v
Tactic:
case _ =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1✝ : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c1 : ¬u = x
c2 : v = x
⊢ V x = a
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : ¬u = x
h✝ : ¬v = x
⊢ V x = V x
Tactic:
case _ =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : v = v
⊢ a = a
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : u = x
h✝ : ¬v = v
⊢ a = V v
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1✝ : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c1 : ¬u = x
c2 : v = x
⊢ V x = a
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1✝ : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
a2 : v ∈ xs
c1 : ¬u = v
⊢ V v = a

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1✝ : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
a2 : v ∈ xs
c1 : ¬u = v
⊢ V v = a
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
h✝¹ : ¬u = x
h✝ : ¬v = x
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ v' ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args

State before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
State after:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset

State before:
case h1.h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
State after:
no goals

State before:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
c1 : X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
simp at c1
State after:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length

State before:
case h1.h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
cases c1
State after:
case h1.h2.intro
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
left✝ : X = hd.name
right✝ : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
case intro c1_left c1_right =>
  simp
  simp only [eq_comm]
  exact c1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = (List.map (fun c => if c = u then a else V c) xs).length
Tactic:
simp
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = xs.length

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ hd.args.length = xs.length
Tactic:
simp only [eq_comm]
State after:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ xs.length = hd.args.length

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : v ∉ xs
h2 : ¬isBoundIn v (def_ X xs)
v' : VarName
a1 : isFreeIn v' hd.q
s1 :
  List.map ((fun a_1 => if a_1 = v then a else V a_1) ∘ fun x => if u = x then v else x) xs =
    List.map (fun a_1 => if a_1 = u then a else V a_1) xs
c1_left : X = hd.name
c1_right : xs.length = hd.args.length
⊢ xs.length = hd.args.length
Tactic:
exact c1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ Holds D I (fun c => if c = u then a else V c) tl (def_ X xs) ↔
    Holds D I (fun c => if c = v then a else V c) tl (def_ X (List.map (fun x => if u = x then v else x) xs))
Tactic:
apply ih
State after:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isFreeIn v (def_ X xs)

case h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isBoundIn v (def_ X xs)

State before:
case h1
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isFreeIn v (def_ X xs)
Tactic:
exact h1
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
u v : VarName
a : D
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    ¬isFreeIn v F →
      ¬isBoundIn v F →
        (Holds D I (Function.updateITE V u a) tl F ↔
          Holds D I (Function.updateITE V v a) tl (Sub.Var.One.Rec.fastReplaceFree u v F))
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if u = x then v else x) xs).length = hd.args.length)
⊢ ¬isBoundIn v (def_ X xs)
Tactic:
exact h2
State after:
no goals