Theorem: FOL.NV.Sub.Prop.All.Rec.substitution_theorem (FOL/NV/Sub/Prop/All/Rec/Sub.lean)

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
τ : PredName → PredName
F : Formula
⊢ Holds D I V E (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V E (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V E F
Tactic:
induction E generalizing F V
State after:
case nil
D : Type
I : Interpretation D
τ : PredName → PredName
V : VarAssignment D
F : Formula
⊢ Holds D I V [] (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] F

case cons
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
F : Formula
⊢ Holds D I V (head✝ :: tail✝) (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) F

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
case nil.def_ X xs =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tl (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tl F
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
case cons.def_ hd tl ih X xs =>
  simp only [Holds] at ih
  simp at ih
  simp only [sub]
  simp only [Holds]
  split_ifs
  case _ c1 =>
    specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
    simp only [sub_no_predVar hd.q τ hd.h2] at ih
    apply ih
  case _ c1 =>
    specialize ih V (def_ X xs)
    simp only [sub] at ih
    exact ih
State after:
no goals

State before:
case cons
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
F : Formula
⊢ Holds D I V (head✝ :: tail✝) (sub τ F) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) F
Tactic:
induction F generalizing V
State after:
case cons.pred_const_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.pred_var_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_var_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.eq_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ a✝ : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (eq_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ true_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) true_

case cons.false_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ false_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_

case cons.not_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ a✝.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) a✝.not_

case cons.imp_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.imp_ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.and_ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.or_ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝¹) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝¹
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (a✝¹.iff_ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (forall_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ a✝) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) a✝
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.def_
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (def_ a✝¹ a✝)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (def_ a✝¹ a✝)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_const_ X xs)
Tactic:
case pred_const_ X xs =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_var_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
case pred_var_ X xs =>
    simp only [sub]
    split_ifs
    case pos c1 =>
      simp only [Holds]
      simp
      simp only [if_pos c1]
    case neg c1 =>
      simp only [Holds]
      simp
      simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (eq_ x y)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Tactic:
case eq_ x y =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ false_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Tactic:
case true_ | false_ =>
  simp only [sub]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
case not_ phi phi_ih =>
  simp only [Holds] at phi_ih
  simp only [sub]
  simp only [Holds]
  congr! 1
  apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ x phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [Holds] at phi_ih
  simp only [sub]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intros d
  apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_const_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_const_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_const_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_const_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (pred_var_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (if xs = [] then pred_var_ (τ X) [] else pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (if xs = [] then pred_var_ (τ X) [] else pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
h✝ : xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ (τ X) []) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)

case neg
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
h✝ : ¬xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ (τ X) []) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
case pos c1 =>
  simp only [Holds]
  simp
  simp only [if_pos c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
case neg c1 =>
  simp only [Holds]
  simp
  simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ (τ X) []) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ I.pred_var_ (τ X) (List.map V []) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ I.pred_var_ (τ X) (List.map V []) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ I.pred_var_ (τ X) [] ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : xs = []
⊢ I.pred_var_ (τ X) [] ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)
Tactic:
simp only [if_pos c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔
    if List.map V xs = [] then I.pred_var_ (τ X) (List.map V []) else I.pred_var_ X (List.map V xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
X : PredName
xs : List VarName
V : VarAssignment D
c1 : ¬xs = []
⊢ I.pred_var_ X (List.map V xs) ↔ if xs = [] then I.pred_var_ (τ X) [] else I.pred_var_ X (List.map V xs)
Tactic:
simp only [if_neg c1]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (eq_ x y)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (eq_ x y) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x y : VarName
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (eq_ x y) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (eq_ x y)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ false_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) false_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) false_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds] at phi_ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi.not_) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi).not_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi).not_ ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi.not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ¬Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ¬Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [Holds] at phi_ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [Holds] at psi_ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (phi.iff_ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) ((sub τ phi).iff_ (sub τ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) ((sub τ phi).iff_ (sub τ psi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (phi.iff_ psi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ (Holds D I V (head✝ :: tail✝) (sub τ phi) ↔ Holds D I V (head✝ :: tail✝) (sub τ psi)) ↔
    (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ (Holds D I V (head✝ :: tail✝) (sub τ phi) ↔ Holds D I V (head✝ :: tail✝) (sub τ psi)) ↔
    (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi

case a.h.e'_2.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) psi

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
phi psi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
psi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) psi
⊢ Holds D I V (head✝ :: tail✝) (sub τ psi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) psi
Tactic:
apply psi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds =>
            if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
V : VarAssignment D
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ x phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)
Tactic:
simp only [Holds] at phi_ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ x phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (sub τ (exists_ x phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (exists_ x (sub τ phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ Holds D I V (head✝ :: tail✝) (exists_ x (sub τ phi)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds =>
          if ds = [] then Holds D I V (head✝ :: tail✝) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (head✝ :: tail✝) (exists_ x phi)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi)) ↔
    ∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x d) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi)) ↔
    ∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (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
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x a) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x a) (head✝ :: tail✝) phi
Tactic:
intros d
State after:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateITE V x d) (head✝ :: tail✝) phi

State before:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply phi_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ (∀ (d : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi)) ↔
    ∀ (d : D),
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ (∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (sub τ phi)) ↔
    ∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
τ : PredName → PredName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tail✝ (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tail✝ (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tail✝ F
x : VarName
phi : Formula
V : VarAssignment D
phi_ih :
  ∀ (V : VarAssignment D),
    Holds D I V (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V (head✝ :: tail✝) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (sub τ phi) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateITE V x a) (head✝ :: tail✝) phi

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V [] (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V [] (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then Holds D I V tl (pred_var_ (τ P) []) else I.pred_var_ P ds }
        V tl F
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds] at ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp at ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [sub]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then Holds D I V (hd :: tl) (pred_var_ (τ P) []) else I.pred_var_ P ds }
      V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ (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
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
⊢ (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
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
        V tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
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
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
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
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
case _ c1 =>
  specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
  simp only [sub_no_predVar hd.q τ hd.h2] at ih
  apply ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
case _ c1 =>
  specialize ih V (def_ X xs)
  simp only [sub] at ih
  exact ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
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
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl (sub τ hd.q) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (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 ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl (sub τ hd.q) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (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 ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
simp only [sub_no_predVar hd.q τ hd.h2] at ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (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 ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      (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 ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply ih
State after:
no goals

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
ih :
  ∀ (V : VarAssignment D) (F : Formula),
    Holds D I V tl (sub τ F) ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
        V tl F
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
specialize ih V (def_ X xs)
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (sub τ (def_ X xs)) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
simp only [sub] at ih
State after:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
τ : PredName → PredName
hd : Definition
tl : List Definition
X : DefName
xs : List VarName
V : VarAssignment D
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
ih :
  Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) [] else I.pred_var_ P ds }
      V tl (def_ X xs)
⊢ Holds D I V tl (def_ X xs) ↔
    Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun P ds => if ds = [] then I.pred_var_ (τ P) (List.map V []) else I.pred_var_ P ds }
      V tl (def_ X xs)
Tactic:
exact ih
State after:
no goals