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

State before:
D : Type
I I' : Interpretation D
V : VarAssignment D
E : Env
F : Formula
h1 : I.pred_const_ = I'.pred_const_
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V E F ↔ Holds D I' V E F
Tactic:
induction E generalizing F V
State after:
case nil
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
V : VarAssignment D
F : Formula
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V [] F ↔ Holds D I' V [] F

case cons
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
F : Formula
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I' V (head✝ :: tail✝) F

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 P ds a1
    simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
    simp only [hd.h2] at a1
    simp at a1
  case neg c1 =>
    apply ih
    intro P ds a1
    simp only [predVarOccursIn] at a1
State after:
no goals

State before:
case cons
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
F : Formula
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I' V (head✝ :: tail✝) F
Tactic:
induction F generalizing V
State after:
case cons.pred_const_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_const_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (eq_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length true_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I' V (head✝ :: tail✝) true_

case cons.false_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length false_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I' V (head✝ :: tail✝) false_

case cons.not_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝.not_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I' V (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.imp_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.and_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.or_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.iff_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (forall_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (exists_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.def_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_const_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (pred_var_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (eq_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length true_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I' V (head✝ :: tail✝) true_

case cons.false_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length false_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I' V (head✝ :: tail✝) false_

case cons.not_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝.not_ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I' V (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.imp_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.and_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.or_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (a✝¹.iff_ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I' V (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (forall_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (exists_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (exists_ a✝¹ a✝)

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

case cons.pred_var_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = a✝¹ ∧ ds.length = a✝.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ a✝¹ (List.map V a✝) ↔ I'.pred_var_ a✝¹ (List.map V a✝)

case cons.not_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ¬Holds D I V (head✝ :: tail✝) a✝ ↔ ¬Holds D I' V (head✝ :: tail✝) a✝

case cons.imp_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length a✝¹ ∨ predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length a✝¹ ∨ predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length a✝¹ ∨ predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝¹ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I' V (head✝ :: tail✝) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length a✝¹ ∨ predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I' V (head✝ :: tail✝) a✝)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length a✝ → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_const_ X (List.map V xs) ↔ I'.pred_const_ X (List.map V xs)
Tactic:
case pred_const_ X xs =>
  simp only [h1]
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X ∧ ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
case pred_var_ X xs =>
  simp at h2
  specialize h2 X (List.map V xs)
  simp at h2
  exact h2
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ¬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 h2
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ 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 =>
  first | apply forall_congr' | apply exists_congr
  intro d
  exact phi_ih (Function.updateITE V x d) h2
State after:
no goals

State before:
case cons.def_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ a✝¹ a✝) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I' V (head✝ :: tail✝) (def_ a✝¹ a✝)
Tactic:
simp only [predVarOccursIn] at h2
State after:
case cons.def_
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_const_ X (List.map V xs) ↔ I'.pred_const_ X (List.map V xs)
Tactic:
simp only [h1]
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X ∧ ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
simp at h2
State after:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X → ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), P = X → ds.length = xs.length → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
specialize h2 X (List.map V xs)
State after:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : X = X → (List.map V xs).length = xs.length → (I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs))
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : X = X → (List.map V xs).length = xs.length → (I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs))
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
simp at h2
State after:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
X : PredName
xs : List VarName
V : VarAssignment D
h2 : I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
⊢ I.pred_var_ X (List.map V xs) ↔ I'.pred_var_ X (List.map V xs)
Tactic:
exact h2
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ¬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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi
Tactic:
exact phi_ih V h2
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi

case a.h.e'_2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
case a.h.e'_1.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)

State before:
case a.h.e'_1.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
State after:
case a.h.e'_1.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length phi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case a.h.e'_1.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length phi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
apply h2
State after:
case a.h.e'_1.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length phi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi

State before:
case a.h.e'_1.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length phi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Tactic:
left
State after:
case a.h.e'_1.a.h2.a.h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length phi
⊢ predVarOccursIn P ds.length phi

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

State before:
case a.h.e'_2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi
Tactic:
apply psi_ih
State after:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)

State before:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
State after:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case a.h.e'_2.a.h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
apply h2
State after:
case a.h.e'_2.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi

State before:
case a.h.e'_2.a.h2.a
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi
Tactic:
right
State after:
case a.h.e'_2.a.h2.a.h
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I' V (head✝ :: tail✝) psi)
V : VarAssignment D
h2 :
  ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length phi ∨ predVarOccursIn P ds.length psi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length psi
⊢ predVarOccursIn P ds.length psi

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

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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:
exact phi_ih (Function.updateITE V x d) h2
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (∃ 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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tail✝ F ↔ Holds D I' V tail✝ F)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I' V (head✝ :: tail✝) phi)
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length phi → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ ∀ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
⊢ (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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 P ds a1
  simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
  simp only [hd.h2] at a1
  simp at a1
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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
  intro P ds a1
  simp only [predVarOccursIn] at a1
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length hd.q → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
State after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length hd.q
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length hd.q
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet P ds.length] at a1
State after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : (P, ds.length) ∈ hd.q.predVarSet
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : (P, ds.length) ∈ hd.q.predVarSet
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [hd.h2] at a1
State after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : (P, ds.length) ∈ ∅
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : X = hd.name ∧ xs.length = hd.args.length
P : PredName
ds : List D
a1 : (P, ds.length) ∈ ∅
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp at a1
State after:
no goals

State before:
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
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 h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length (def_ X xs) → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
Tactic:
intro P ds a1
State after:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length (def_ X xs)
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds

State before:
case h2
D : Type
I I' : Interpretation D
h1 : I.pred_const_ = I'.pred_const_
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    (∀ (P : PredName) (ds : List D), predVarOccursIn P ds.length F → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)) →
      (Holds D I V tl F ↔ Holds D I' V tl F)
X : DefName
xs : List VarName
V : VarAssignment D
h2 : ∀ (P : PredName) (ds : List D), False → (I.pred_var_ P ds ↔ I'.pred_var_ P ds)
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
P : PredName
ds : List D
a1 : predVarOccursIn P ds.length (def_ X xs)
⊢ I.pred_var_ P ds ↔ I'.pred_var_ P ds
Tactic:
simp only [predVarOccursIn] at a1
State after:
no goals