Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux (FOL/NV/Sub/Var/One/Rec/Admits.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
v t : VarName
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) E F ↔ Holds D I V E (fastReplaceFree v t F)
Tactic:
induction E generalizing F binders V
State after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
V : VarAssignment D
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) [] F ↔ Holds D I V [] (fastReplaceFree v t F)

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) F ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t F)

State before:
case cons
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
F : Formula
h1 : fastAdmitsAux v t binders F
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) F ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t F)
Tactic:
induction F generalizing binders V
State after:
case cons.pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (pred_const_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (pred_const_ a✝¹ a✝))

case cons.pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (pred_var_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (pred_var_ a✝¹ a✝))

case cons.eq_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (eq_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (eq_ a✝¹ a✝))

case cons.true_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders true_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) true_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t true_)

case cons.false_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders false_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) false_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t false_)

case cons.not_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝.not_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝.not_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝.not_)

case cons.imp_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.imp_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.imp_ a✝))

case cons.and_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.and_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.and_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.and_ a✝))

case cons.or_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.or_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.or_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.or_ a✝))

case cons.iff_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.iff_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.iff_ a✝))

case cons.forall_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (forall_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (forall_ a✝¹ a✝))

case cons.exists_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (exists_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (exists_ a✝¹ a✝))

case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (def_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))

State before:
case cons.pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (pred_const_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (pred_const_ a✝¹ a✝))

case cons.pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (pred_var_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (pred_var_ a✝¹ a✝))

case cons.eq_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (eq_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (eq_ a✝¹ a✝))

case cons.true_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders true_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) true_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t true_)

case cons.false_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders false_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) false_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t false_)

case cons.not_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝.not_
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝.not_ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝.not_)

case cons.imp_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.imp_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.imp_ a✝))

case cons.and_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.and_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.and_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.and_ a✝))

case cons.or_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.or_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.or_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.or_ a✝))

case cons.iff_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (a✝¹.iff_ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (a✝¹.iff_ a✝))

case cons.forall_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (forall_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (forall_ a✝¹ a✝))

case cons.exists_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (exists_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (exists_ a✝¹ a✝))

case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (def_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
all_goals
  simp only [fastAdmitsAux] at h1
  simp only [fastReplaceFree]
  simp only [Holds]
State after:
case cons.pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_const_ a✝¹ (List.map (Function.updateITE V v (V' t)) a✝) ↔
    I.pred_const_ a✝¹ (List.map V (List.map (fun x => if v = x then t else x) a✝))

case cons.pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ a✝¹ (List.map (Function.updateITE V v (V' t)) a✝) ↔
    I.pred_var_ a✝¹ (List.map V (List.map (fun x => if v = x then t else x) a✝))

case cons.eq_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = a✝¹ ∨ v = a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Function.updateITE V v (V' t) a✝¹ = Function.updateITE V v (V' t) a✝ ↔
    V (if v = a✝¹ then t else a✝¹) = V (if v = a✝ then t else a✝)

case cons.not_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ ¬Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
    ¬Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝)

case cons.imp_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝¹ ∧ fastAdmitsAux v t binders a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ →
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹) → Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝)

case cons.and_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝¹ ∧ fastAdmitsAux v t binders a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ∧
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹) ∧ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝)

case cons.or_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝¹ ∧ fastAdmitsAux v t binders a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ∨
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹) ∨ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝)

case cons.iff_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝¹ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders a✝¹ ∧ fastAdmitsAux v t binders a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝¹ ↔
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝) ↔
    (Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝¹) ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))

case cons.forall_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : v = a✝¹ ∨ fastAdmitsAux v t (binders ∪ {a✝¹}) a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V v (V' t)) a✝¹ d) (head✝ :: tail✝) a✝) ↔
    Holds D I V (head✝ :: tail✝) (if v = a✝¹ then forall_ a✝¹ a✝ else forall_ a✝¹ (fastReplaceFree v t a✝))

case cons.exists_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders a✝ →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) a✝ ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t a✝))
V : VarAssignment D
binders : Finset VarName
h1 : v = a✝¹ ∨ fastAdmitsAux v t (binders ∪ {a✝¹}) a✝
h2 : ∀ v ∉ binders, V' v = V v
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) a✝¹ d) (head✝ :: tail✝) a✝) ↔
    Holds D I V (head✝ :: tail✝) (if v = a✝¹ then exists_ a✝¹ a✝ else exists_ a✝¹ (fastReplaceFree v t a✝))

case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v (V' t)) head✝.args
          (List.map (Function.updateITE V v (V' t)) a✝))
        tail✝ head✝.q
    else Holds D I (Function.updateITE V v (V' t)) tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ (List.map (fun x => if v = x then t else x) a✝).length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V (List.map (fun x => if v = x then t else x) a✝))) tail✝
        head✝.q
    else Holds D I V tail✝ (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map V (List.map (fun x => if v = x then t else x) xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  simp
  congr! 1
  simp only [List.map_eq_map_iff]
  intro x a1
  simp
  simp only [Function.updateITE]
  split_ifs
  case _ c1 c2 =>
    subst c1
    tauto
  case _ c1 c2 =>
    subst c1
    contradiction
  case _ c1 c2 =>
    subst c2
    contradiction
  case _ c1 c2 =>
    rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Function.updateITE V v (V' t) x = Function.updateITE V v (V' t) y ↔
    V (if v = x then t else x) = V (if v = y then t else y)
Tactic:
case eq_ x y =>
  simp only [Function.updateITE]
  simp only [eq_comm]
  congr! 1
  all_goals
    split_ifs
    case _ c1 =>
      subst c1
      tauto
    case _ c1 =>
      rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ ¬Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    ¬Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V binders h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  split_ifs
  case _ c1 =>
    subst c1
    simp only [Holds]
    first | apply forall_congr' | apply exists_congr
    intro d
    congr! 1
    funext x
    simp only [Function.updateITE]
    split_ifs <;> rfl
  case _ c1 =>
    simp only [Holds]
    first | apply forall_congr' | apply exists_congr
    intro d
    cases h1
    case inl h1 =>
      contradiction
    case inr h1 =>
      simp only [Function.updateITE_comm V v x d (V' t) c1]
      apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
      simp only [Function.updateITE]
      simp
      push_neg
      intros v' a1 a2
      simp only [if_neg a2]
      exact h2 v' a1
State after:
no goals

State before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (def_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastAdmitsAux] at h1
State after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))

State before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastReplaceFree]
State after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

State before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Tactic:
simp only [Holds]
State after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v (V' t)) head✝.args
          (List.map (Function.updateITE V v (V' t)) a✝))
        tail✝ head✝.q
    else Holds D I (Function.updateITE V v (V' t)) tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ (List.map (fun x => if v = x then t else x) a✝).length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V (List.map (fun x => if v = x then t else x) a✝))) tail✝
        head✝.q
    else Holds D I V tail✝ (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map V (List.map (fun x => if v = x then t else x) xs))
Tactic:
simp
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map (V ∘ fun x => if v = x then t else x) xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map (V ∘ fun x => if v = x then t else x) xs)
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ List.map (Function.updateITE V v (V' t)) xs = List.map (V ∘ fun x => if v = x then t else x) xs

State before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ List.map (Function.updateITE V v (V' t)) xs = List.map (V ∘ fun x => if v = x then t else x) xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ∀ x ∈ xs, Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ∀ x ∈ xs, Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Tactic:
intro x a1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Tactic:
simp
State after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = V (if v = x then t else x)

State before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = V (if v = x then t else x)
Tactic:
simp only [Function.updateITE]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ (if x = v then V' t else V x) = V (if v = x then t else x)

State before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ (if x = v then V' t else V x) = V (if v = x then t else x)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : x = v
h✝ : v = x
⊢ V' t = V t

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : x = v
h✝ : ¬v = x
⊢ V' t = V x

case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : ¬x = v
h✝ : v = x
⊢ V x = V t

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : ¬x = v
h✝ : ¬v = x
⊢ V x = V x

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : v = x
⊢ V' t = V t
Tactic:
case _ c1 c2 =>
  subst c1
  tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : ¬v = x
⊢ V' t = V x
Tactic:
case _ c1 c2 =>
  subst c1
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : v = x
⊢ V x = V t
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : ¬v = x
⊢ V x = V x
Tactic:
case _ c1 c2 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : v = x
⊢ V' t = V t
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : x = x
⊢ V' t = V t

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : x = x
⊢ V' t = V t
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : ¬v = x
⊢ V' t = V x
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : ¬x = x
⊢ V' t = V x

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : ¬x = x
⊢ V' t = V x
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : v = x
⊢ V x = V t
Tactic:
subst c2
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a1 : v ∈ xs
c1 : ¬v = v
⊢ V v = V t

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a1 : v ∈ xs
c1 : ¬v = v
⊢ V v = V t
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : ¬v = x
⊢ V x = V x
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Function.updateITE V v (V' t) x = Function.updateITE V v (V' t) y ↔
    V (if v = x then t else x) = V (if v = y then t else y)
Tactic:
simp only [Function.updateITE]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ((if x = v then V' t else V x) = if y = v then V' t else V y) ↔
    V (if v = x then t else x) = V (if v = y then t else y)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ((if x = v then V' t else V x) = if y = v then V' t else V y) ↔
    V (if v = x then t else x) = V (if v = y then t else y)
Tactic:
simp only [eq_comm]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ((if v = x then V' t else V x) = if v = y then V' t else V y) ↔
    V (if v = x then t else x) = V (if v = y then t else y)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ((if v = x then V' t else V x) = if v = y then V' t else V y) ↔
    V (if v = x then t else x) = V (if v = y then t else y)
Tactic:
congr! 1
State after:
case a.h.e'_2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if v = x then V' t else V x) = V (if v = x then t else x)

case a.h.e'_3
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if v = y then V' t else V y) = V (if v = y then t else y)

State before:
case a.h.e'_2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if v = x then V' t else V x) = V (if v = x then t else x)

case a.h.e'_3
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if v = y then V' t else V y) = V (if v = y then t else y)
Tactic:
all_goals
  split_ifs
  case _ c1 =>
    subst c1
    tauto
  case _ c1 =>
    rfl
State after:
no goals

State before:
case a.h.e'_3
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if v = y then V' t else V y) = V (if v = y then t else y)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
h✝ : v = y
⊢ V' t = V t

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
h✝ : ¬v = y
⊢ V y = V y

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : v = y
⊢ V' t = V t
Tactic:
case _ c1 =>
  subst c1
  tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = y
⊢ V y = V y
Tactic:
case _ c1 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : v = y
⊢ V' t = V t
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = x ∨ v = v → t ∉ binders
⊢ V' t = V t

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = x ∨ v = v → t ∉ binders
⊢ V' t = V t
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ v = y → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = y
⊢ V y = V y
Tactic:
rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ ¬Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    ¬Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
exact phi_ih V binders h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi ∧ fastAdmitsAux v t binders psi
h2 : ∀ v ∉ binders, V' v = V v
⊢ (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi) ↔
    (Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi) ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
left✝ : fastAdmitsAux v t binders phi
right✝ : fastAdmitsAux v t binders psi
⊢ (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi) ↔
    (Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi) ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1_left : fastAdmitsAux v t binders phi
h1_right : fastAdmitsAux v t binders psi
⊢ (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi) ↔
    (Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi) ↔ Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1_left : fastAdmitsAux v t binders phi
h1_right : fastAdmitsAux v t binders psi
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1_left : fastAdmitsAux v t binders phi
h1_right : fastAdmitsAux v t binders psi
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1_left : fastAdmitsAux v t binders phi
h1_right : fastAdmitsAux v t binders psi
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
exact phi_ih V binders h1_left h2
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders psi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1_left : fastAdmitsAux v t binders phi
h1_right : fastAdmitsAux v t binders psi
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) psi ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t psi)
Tactic:
exact psi_ih V binders h1_right h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
h✝ : v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x phi)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
h✝ : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x (fastReplaceFree v t phi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x phi)
Tactic:
case _ c1 =>
  subst c1
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  congr! 1
  funext x
  simp only [Function.updateITE]
  split_ifs <;> rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x (fastReplaceFree v t phi))
Tactic:
case _ c1 =>
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  cases h1
  case inl h1 =>
    contradiction
  case inr h1 =>
    simp only [Function.updateITE_comm V v x d (V' t) c1]
    apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
    simp only [Function.updateITE]
    simp
    push_neg
    intros v' a1 a2
    simp only [if_neg a2]
    exact h2 v' a1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x phi)
Tactic:
subst c1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ v phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ v phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
congr! 1
State after:
case h.a.h.e'_3
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d = Function.updateITE V v d

State before:
case h.a.h.e'_3
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d = Function.updateITE V v d
Tactic:
funext x
State after:
case h.a.h.e'_3.h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
x : VarName
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d x = Function.updateITE V v d x

State before:
case h.a.h.e'_3.h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
x : VarName
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d x = Function.updateITE V v d x
Tactic:
simp only [Function.updateITE]
State after:
case h.a.h.e'_3.h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
x : VarName
⊢ (if x = v then d else if x = v then V' t else V x) = if x = v then d else V x

State before:
case h.a.h.e'_3.h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
d : D
x : VarName
⊢ (if x = v then d else if x = v then V' t else V x) = if x = v then d else V x
Tactic:
split_ifs <;> rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x (fastReplaceFree v t phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
cases h1
State after:
case h.inl
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h✝ : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

case h.inr
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h✝ : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
case inl h1 =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
case inr h1 =>
  simp only [Function.updateITE_comm V v x d (V' t) c1]
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  simp only [Function.updateITE]
  simp
  push_neg
  intros v' a1 a2
  simp only [if_neg a2]
  exact h2 v' a1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
simp only [Function.updateITE_comm V v x d (V' t) c1]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders ∪ {x}, V' v = Function.updateITE V x d v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders ∪ {x}, V' v = Function.updateITE V x d v
Tactic:
simp only [Function.updateITE]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders ∪ {x}, V' v = if v = x then d else V v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders ∪ {x}, V' v = if v = x then d else V v
Tactic:
simp
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders, ¬v = x → V' v = if v = x then d else V v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders, ¬v = x → V' v = if v = x then d else V v
Tactic:
push_neg
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders, v ≠ x → V' v = if v = x then d else V v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders, v ≠ x → V' v = if v = x then d else V v
Tactic:
intros v' a1 a2
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
v' : VarName
a1 : v' ∉ binders
a2 : v' ≠ x
⊢ V' v' = if v' = x then d else V v'

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
v' : VarName
a1 : v' ∉ binders
a2 : v' ≠ x
⊢ V' v' = if v' = x then d else V v'
Tactic:
simp only [if_neg a2]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
v' : VarName
a1 : v' ∉ binders
a2 : v' ≠ x
⊢ V' v' = V v'

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
v' : VarName
a1 : v' ∉ binders
a2 : v' ≠ x
⊢ V' v' = V v'
Tactic:
exact h2 v' a1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v (V' t)) hd.args (List.map (Function.updateITE V v (V' t)) xs))
        tl hd.q
    else Holds D I (Function.updateITE V v (V' t)) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if v = x then t else x) xs))) tl hd.q
    else Holds D I V tl (def_ X (List.map (fun x => if v = x then t else x) xs))
Tactic:
unfold Function.updateITE
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I
        (Function.updateListITE (fun c => if c = v then V' t else V c) hd.args
          (List.map (fun c => if c = v then V' t else V c) xs))
        tl hd.q
    else Holds D I (fun c => if c = v then V' t else V c) tl (def_ X xs)) ↔
    if X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if v = x then t else x) xs))) tl hd.q
    else Holds D I V tl (def_ X (List.map (fun x => if v = x then t else x) xs))

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

case a.h₂.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = v then V' t else V c) hd.args
        (List.map (fun c => if c = v then V' t else V c) xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if v = x then t else x) xs))) tl hd.q

case a.h₃.a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ Holds D I (fun c => if c = v then V' t else V c) tl (def_ X xs) ↔
    Holds D I V tl (def_ X (List.map (fun x => if v = x then t else x) xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ X = hd.name ∧ xs.length = hd.args.length ↔
    X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
Tactic:
case _ =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ X = hd.name ∧ xs.length = hd.args.length ↔
    X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
⊢ Holds D I
      (Function.updateListITE (fun c => if c = v then V' t else V c) hd.args
        (List.map (fun c => if c = v then V' t else V c) xs))
      tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V (List.map (fun x => if v = x then t else x) xs))) tl hd.q
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
⊢ ∀ (v_1 : VarName),
    isFreeIn v_1 hd.q →
      Function.updateListITE (fun c => if c = v then V' t else V c) hd.args
          (List.map (fun c => if c = v then V' t else V c) xs) v_1 =
        Function.updateListITE V hd.args (List.map V (List.map (fun x => if v = x then t else x) xs)) v_1

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

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

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if c = v then V' t else V c) hd.args
      (List.map (fun c => if c = v then V' t else V c) xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if v = x then t else x) xs) v'
Tactic:
simp only [eq_comm]
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ Function.updateListITE (fun c => if v = c then V' t else V c) hd.args
      (List.map (fun c => if v = c then V' t else V c) xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if v = x then t else x) xs) v'

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

case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ Function.updateListITE (fun c => if v = c then V' t else V c) hd.args
      (List.map (fun c => if v = c then V' t else V c) xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if v = x then t else x) xs) v'

State before:
case s1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
⊢ List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs

case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ Function.updateListITE (fun c => if v = c then V' t else V c) hd.args
      (List.map (fun c => if v = c then V' t else V c) xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if v = x then t else x) xs) v'
Tactic:
{
  simp only [List.map_eq_map_iff]
  intro x a2
  simp
  split_ifs
  case _ c2 =>
    apply h2
    subst c2
    exact h1 a2
  case _ c2 =>
    rfl
}
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ Function.updateListITE (fun c => if v = c then V' t else V c) hd.args
      (List.map (fun c => if v = c then V' t else V c) xs) v' =
    Function.updateListITE V hd.args (List.map (V ∘ fun x => if v = x then t else x) xs) v'

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

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

case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length

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

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

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

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

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

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c2 : v = x
⊢ V' t = V t
Tactic:
case _ c2 =>
  apply h2
  subst c2
  exact h1 a2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c2 : ¬v = x
⊢ V x = V x
Tactic:
case _ c2 =>
  rfl
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c2 : v = x
⊢ V' t = V t
Tactic:
apply h2
State after:
case a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c2 : v = x
⊢ t ∉ binders

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

State before:
case a
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
a2 : v ∈ xs
⊢ t ∉ binders
Tactic:
exact h1 a2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
x : VarName
a2 : x ∈ xs
c2 : ¬v = x
⊢ V x = V x
Tactic:
rfl
State after:
no goals

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

State before:
case h1.h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) 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
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
a1 : v' ∈ hd.q.freeVarSet
⊢ v' ∈ hd.args.toFinset

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

State before:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
c1 : X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length
Tactic:
simp at c1
State after:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = (List.map (V ∘ fun x => if v = x then t else x) xs).length

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

State before:
case h1.h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
v' : VarName
a1 : isFreeIn v' hd.q
s1 : List.map (fun x => if v = x then V' t else V x) xs = List.map (V ∘ fun x => if v = x then t else x) xs
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ hd.args.length = xs.length
Tactic:
tauto
State after:
no goals

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

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ ∀ v ∉ binders, V' v = V v

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ fastAdmitsAux v t binders (def_ X xs)
Tactic:
simp only [fastAdmitsAux]
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ v ∈ xs → t ∉ binders

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ v ∈ xs → t ∉ binders
Tactic:
exact h1
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tl F ↔ Holds D I V tl (fastReplaceFree v t F))
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
a✝ : ¬(X = hd.name ∧ (List.map (fun x => if v = x then t else x) xs).length = hd.args.length)
⊢ ∀ v ∉ binders, V' v = V v
Tactic:
exact h2
State after:
no goals