Theorem: FOL.NV.Holds_coincide_Var (FOL/NV/Semantics.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V E F ↔ Holds D I V' E F
Tactic:
induction E generalizing F V V'
State after:
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V [] F ↔ Holds D I V' [] F

case cons
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : VarName), isFreeIn v F → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) F

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
    else Holds D I V' tl (def_ X xs)
Tactic:
case cons.def_ hd tl ih X xs =>
  split_ifs
  case pos c1 =>
    apply ih
    intro v a1
    simp only [isFreeIn_iff_mem_freeVarSet v hd.q] at a1
    have s1 : v ∈ List.toFinset hd.args
    apply Finset.mem_of_subset hd.h1 a1
    simp only [List.mem_toFinset] at s1
    apply Function.updateListITE_fun_coincide_mem_eq_len V V' hd.args xs v h1 s1
    tauto
  case neg c1 =>
    apply ih
    tauto
State after:
no goals

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

case cons.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (pred_var_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (eq_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v true_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v false_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝.not_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.imp_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.and_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.or_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.iff_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (forall_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (exists_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

State before:
case cons.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (pred_const_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (pred_var_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (eq_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v true_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v false_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝.not_ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.imp_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.and_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.or_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.iff_ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (forall_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (exists_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
all_goals
  simp only [isFreeIn] at h1
  simp only [Holds]
State after:
case cons.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ I.pred_const_ a✝¹ (List.map V a✝) ↔ I.pred_const_ a✝¹ (List.map V' a✝)

case cons.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ I.pred_var_ a✝¹ (List.map V a✝) ↔ I.pred_var_ a✝¹ (List.map V' a✝)

case cons.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), v = a✝¹ ∨ v = a✝ → V v = V' v
⊢ V a✝¹ = V a✝ ↔ V' a✝¹ = V' a✝

case cons.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝ → V v = V' v
⊢ ¬Holds D I V (head✝ :: tail✝) a✝ ↔ ¬Holds D I V' (head✝ :: tail✝) a✝

case cons.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) a✝¹ → Holds D I V (head✝ :: tail✝) a✝ ↔
    Holds D I V' (head✝ :: tail✝) a✝¹ → Holds D I V' (head✝ :: tail✝) a✝

case cons.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) a✝¹ ∧ Holds D I V (head✝ :: tail✝) a✝ ↔
    Holds D I V' (head✝ :: tail✝) a✝¹ ∧ Holds D I V' (head✝ :: tail✝) a✝

case cons.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) a✝¹ ∨ Holds D I V (head✝ :: tail✝) a✝ ↔
    Holds D I V' (head✝ :: tail✝) a✝¹ ∨ Holds D I V' (head✝ :: tail✝) a✝

case cons.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝¹ → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → V v = V' v
⊢ (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V (head✝ :: tail✝) a✝) ↔
    (Holds D I V' (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) a✝)

case cons.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → V v = V' v
⊢ (∀ (d : D), Holds D I (Function.updateITE V a✝¹ d) (head✝ :: tail✝) a✝) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' a✝¹ d) (head✝ :: tail✝) a✝

case cons.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v a✝ → V v = V' v) → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) a✝)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V a✝¹ d) (head✝ :: tail✝) a✝) ↔
    ∃ d, Holds D I (Function.updateITE V' a✝¹ d) (head✝ :: tail✝) a✝

case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V a✝)) tail✝ head✝.q
    else Holds D I V tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V' head✝.args (List.map V' a✝)) tail✝ head✝.q
    else Holds D I V' tail✝ (def_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' xs)
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), v = x ∨ v = y → V v = V' v
⊢ V x = V y ↔ V' x = V' y
Tactic:
case eq_ x y =>
  simp at h1
  cases h1
  case intro h1_left h1_right =>
    congr! 1
State after:
no goals

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

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp at h1
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih
  intro v a1
  simp only [Function.updateITE]
  split_ifs <;> tauto
State after:
no goals

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

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

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' xs)
Tactic:
congr! 1
State after:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ List.map V xs = List.map V' xs

State before:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ List.map V xs = List.map V' xs
Tactic:
simp only [List.map_eq_map_iff]
State after:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ ∀ x ∈ xs, V x = V' x

State before:
case a.h.e'_4
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ ∀ x ∈ xs, V x = V' x
Tactic:
exact h1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), v = x ∨ v = y → V v = V' v
⊢ V x = V y ↔ V' x = V' y
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : V x = V' x ∧ V y = V' y
⊢ V x = V y ↔ V' x = V' y

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1 : V x = V' x ∧ V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
left✝ : V x = V' x
right✝ : V y = V' y
⊢ V x = V y ↔ V' x = V' y

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1_left : V x = V' x
h1_right : V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
case intro h1_left h1_right =>
  congr! 1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x y : VarName
V V' : VarAssignment D
h1_left : V x = V' x
h1_right : V y = V' y
⊢ V x = V y ↔ V' x = V' y
Tactic:
congr! 1
State after:
no goals

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

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

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V (head✝ :: tail✝) psi) ↔
    (Holds D I V' (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) psi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi

case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi
Tactic:
apply phi_ih V V'
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v phi → V v = V' v

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v phi → V v = V' v
Tactic:
intro v a1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ V v = V' v

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ V v = V' v
Tactic:
apply h1
State after:
case a.h.e'_1.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi

State before:
case a.h.e'_1.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
left
State after:
case a.h.e'_1.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi

State before:
case a.h.e'_1.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ isFreeIn v phi
Tactic:
exact a1
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi
Tactic:
apply psi_ih V V'
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v psi → V v = V' v

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v psi → V v = V' v
Tactic:
intro v a1
State after:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ V v = V' v

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ V v = V' v
Tactic:
apply h1
State after:
case a.h.e'_2.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi

State before:
case a.h.e'_2.a.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v phi ∨ isFreeIn v psi
Tactic:
right
State after:
case a.h.e'_2.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi

State before:
case a.h.e'_2.a.a.h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v psi
⊢ isFreeIn v psi
Tactic:
exact a1
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x ∧ isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔ Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE V x d v = Function.updateITE V' x d v

State before:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
⊢ ∀ (v : VarName), isFreeIn v phi → Function.updateITE V x d v = Function.updateITE V' x d v
Tactic:
intro v a1
State after:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V x d v = Function.updateITE V' x d v

State before:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
v : VarName
a1 : isFreeIn v phi
⊢ Function.updateITE V x d v = Function.updateITE V' x d v
Tactic:
simp only [Function.updateITE]
State after:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then d else V v) = if v = x then d else V' v

State before:
case h.h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
d : D
v : VarName
a1 : isFreeIn v phi
⊢ (if v = x then d else V v) = if v = x then d else V' v
Tactic:
split_ifs <;> tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' x d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), ¬v = x → isFreeIn v phi → V v = V' v
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' x a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
    else Holds D I V' tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q

case neg
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
Tactic:
case pos c1 =>
  apply ih
  intro v a1
  simp only [isFreeIn_iff_mem_freeVarSet v hd.q] at a1
  have s1 : v ∈ List.toFinset hd.args
  apply Finset.mem_of_subset hd.h1 a1
  simp only [List.mem_toFinset] at s1
  apply Function.updateListITE_fun_coincide_mem_eq_len V V' hd.args xs v h1 s1
  tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)
Tactic:
case neg c1 =>
  apply ih
  tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' xs)) tl hd.q
Tactic:
apply ih
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
intro v a1
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet v hd.q] at a1
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
have s1 : v ∈ List.toFinset hd.args
State after:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case s1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
apply Finset.mem_of_subset hd.h1 a1
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args.toFinset
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
simp only [List.mem_toFinset] at s1
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' xs) v
Tactic:
apply Function.updateListITE_fun_coincide_mem_eq_len V V' hd.args xs v h1 s1
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ hd.args.length = xs.length

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : X = hd.name ∧ xs.length = hd.args.length
v : VarName
a1 : v ∈ hd.q.freeVarSet
s1 : v ∈ hd.args
⊢ hd.args.length = xs.length
Tactic:
tauto
State after:
no goals

State before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ X xs)
Tactic:
apply ih
State after:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (v : VarName), isFreeIn v (def_ X xs) → V v = V' v

State before:
case h1
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tl F ↔ Holds D I V' tl F)
X : DefName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (v : VarName), isFreeIn v (def_ X xs) → V v = V' v
Tactic:
tauto
State after:
no goals