Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux (FOL/NV/Sub/Pred/All/Rec/Option/Sub.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
binders : Finset VarName
F : Formula
h1 : admitsAux τ binders F
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E F ↔
    Holds D I V E (replace c τ F)
Tactic:
induction F generalizing binders V
State after:
case pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (pred_const_ a✝¹ a✝))

case pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_var_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (pred_var_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders true_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E true_ ↔
    Holds D I V E (replace c τ true_)

case false_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace c τ false_)

case not_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders a✝.not_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E a✝.not_ ↔
    Holds D I V E (replace c τ a✝.not_)

case imp_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝¹ ↔
          Holds D I V E (replace c τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.imp_ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (a✝¹.imp_ a✝) ↔
    Holds D I V E (replace c τ (a✝¹.imp_ a✝))

case and_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝¹ ↔
          Holds D I V E (replace c τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.and_ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (a✝¹.and_ a✝) ↔
    Holds D I V E (replace c τ (a✝¹.and_ a✝))

case or_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝¹ ↔
          Holds D I V E (replace c τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.or_ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (a✝¹.or_ a✝) ↔
    Holds D I V E (replace c τ (a✝¹.or_ a✝))

case iff_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝¹ ↔
          Holds D I V E (replace c τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.iff_ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (a✝¹.iff_ a✝) ↔
    Holds D I V E (replace c τ (a✝¹.iff_ a✝))

case forall_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (forall_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (forall_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (forall_ a✝¹ a✝))

case exists_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E a✝ ↔
          Holds D I V E (replace c τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (exists_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (def_ a✝¹ a✝) ↔
    Holds D I V E (replace c τ (def_ a✝¹ a✝))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace c τ (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace c τ (eq_ x y))
Tactic:
case eq_ x y =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace c τ false_)
Tactic:
case true_ | false_ =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi.not_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
case not_ phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  congr! 1
  exact phi_ih V binders h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ x phi)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace c τ (exists_ x phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  intro v a1
  simp only [Function.updateITE]
  simp at a1
  push_neg at a1
  cases a1
  case h.intro a1_left a1_right =>
    simp only [if_neg a1_right]
    exact h2 v a1_left
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (replace c τ (pred_const_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_var_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    if xs.length = ((τ X xs.length).get ⋯).1.length then
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
    else True
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    if xs.length = ((τ X xs.length).get ⋯).1.length then
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
    else True
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E (replace c τ (pred_var_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (pred_var_ X xs) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ (if h : (τ X (List.map V xs).length).isSome = true then
      if (List.map V xs).length = ((τ X (List.map V xs).length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X (List.map V xs).length).get ⋯).1 (List.map V xs)) E
          ((τ X (List.map V xs).length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ (if h : (τ X (List.map V xs).length).isSome = true then
      if (List.map V xs).length = ((τ X (List.map V xs).length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X (List.map V xs).length).get ⋯).1 (List.map V xs)) E
          ((τ X (List.map V xs).length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
⊢ (if h : (τ X xs.length).isSome = true then
      if xs.length = ((τ X xs.length).get ⋯).1.length then
        Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2
      else I.pred_var_ X (List.map V xs)
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if h : (τ X xs.length).isSome = true then
        if xs.length = ((τ X xs.length).get ⋯).1.length then
          Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2
        else pred_var_ X xs
      else pred_var_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
h✝¹ : (τ X xs.length).isSome = true
h✝ : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
h✝¹ : (τ X xs.length).isSome = true
h✝ : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
h✝ : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
case _ c1 c2 =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
case _ c1 =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let opt := τ X xs.length
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let val := Option.get opt c1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let zs := val.fst
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
let H := val.snd
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
obtain s1 := Sub.Var.All.Rec.Fresh.substitution_theorem D I V E (Function.updateListITE id zs xs) c H
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (V ∘ Function.updateListITE id zs xs) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (V ∘ Function.updateListITE id zs xs) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp only [Function.updateListITE_comp] at s1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE (V ∘ id) zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE (V ∘ id) zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp at s1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I V E
      (Var.All.Rec.Fresh.sub (Function.updateListITE id ((τ X xs.length).get ⋯).1 xs) c ((τ X xs.length).get ⋯).2)
Tactic:
simp only [s1]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ Holds D I (Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs)) E ((τ X xs.length).get ⋯).2 ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ ∀ (v : VarName),
    isFreeIn v ((τ X xs.length).get ⋯).2 →
      Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v =
        Function.updateListITE V zs (List.map V xs) v

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
⊢ ∀ (v : VarName),
    isFreeIn v ((τ X xs.length).get ⋯).2 →
      Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v =
        Function.updateListITE V zs (List.map V xs) v
Tactic:
intro v a1
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
by_cases c3 : v ∈ zs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v

State before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
apply Function.updateListITE_mem_eq_len V' V v zs (List.map V xs) c3
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = (List.map V xs).length

State before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Tactic:
simp
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = xs.length

State before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∈ zs
⊢ zs.length = xs.length
Tactic:
simp only [← c2]
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = Function.updateListITE V zs (List.map V xs) v
Tactic:
simp only [Function.updateListITE_not_mem V v zs (List.map V xs) c3]
State after:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = V v

State before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ Function.updateListITE V' ((τ X xs.length).get ⋯).1 (List.map V xs) v = V v
Tactic:
simp only [Function.updateListITE_not_mem V' v zs (List.map V xs) c3]
State after:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ V' v = V v

State before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ V' v = V v
Tactic:
apply h2
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ v ∉ binders

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
⊢ v ∉ binders
Tactic:
intro contra
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
contra : v ∈ binders
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
a1 : isFreeIn v ((τ X xs.length).get ⋯).2
c3 : v ∉ zs
contra : v ∈ binders
⊢ False
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
⊢ False
Tactic:
simp only [Finset.eq_empty_iff_forall_not_mem] at h1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp only [c1] at h1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp only [← c2] at h1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    True → ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    True → ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp at h1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : ∀ x ∈ binders, x ∈ ((τ X xs.length).get ⋯).2.freeVarSet → x ∈ ((τ X xs.length).get ⋯).1
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : ∀ x ∈ binders, x ∈ ((τ X xs.length).get ⋯).2.freeVarSet → x ∈ ((τ X xs.length).get ⋯).1
⊢ False
Tactic:
specialize h1 v contra a1
State after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : v ∈ ((τ X xs.length).get ⋯).1
⊢ False

State before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : v ∈ ((τ X xs.length).get ⋯).1
⊢ False
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace c τ (eq_ x y))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (eq_ x y)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (eq_ x y)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace c τ false_)
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi.not_
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi).not_

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi).not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
    ¬Holds D I V E (replace c τ phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
    ¬Holds D I V E (replace c τ phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi ↔
    Holds D I V E (replace c τ phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi ↔
    Holds D I V E (replace c τ phi)
Tactic:
exact phi_ih V binders h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (phi.iff_ psi)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (phi.iff_ psi) ↔
    Holds D I V E (replace c τ (phi.iff_ psi))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (phi.iff_ psi) ↔
    Holds D I V E (replace c τ (phi.iff_ psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (phi.iff_ psi) ↔
    Holds D I V E (replace c τ (phi.iff_ psi))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (phi.iff_ psi) ↔
    Holds D I V E ((replace c τ phi).iff_ (replace c τ psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (phi.iff_ psi) ↔
    Holds D I V E ((replace c τ phi).iff_ (replace c τ psi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E psi) ↔
    (Holds D I V E (replace c τ phi) ↔ Holds D I V E (replace c τ psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E psi) ↔
    (Holds D I V E (replace c τ phi) ↔ Holds D I V E (replace c τ psi))
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
left✝ : admitsAux τ binders phi
right✝ : admitsAux τ binders psi
⊢ (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E psi) ↔
    (Holds D I V E (replace c τ phi) ↔ Holds D I V E (replace c τ psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ (Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E phi ↔
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V E psi) ↔
    (Holds D I V E (replace c τ phi) ↔ Holds D I V E (replace c τ psi))
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi ↔
    Holds D I V E (replace c τ phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E psi ↔
    Holds D I V E (replace c τ psi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi ↔
    Holds D I V E (replace c τ phi)
Tactic:
exact phi_ih V binders h1_left h2
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E psi ↔
          Holds D I V E (replace c τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E psi ↔
    Holds D I V E (replace c τ psi)
Tactic:
exact psi_ih V binders h1_right h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ x phi)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace c τ (exists_ x phi))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace c τ (exists_ x phi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (replace c τ (exists_ x phi))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (exists_ x (replace c τ phi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (exists_ x phi) ↔
    Holds D I V E (exists_ x (replace c τ phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace c τ phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ∀ (a : D),
    Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ∀ (a : D),
    Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace c τ phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, V' x_1 = Function.updateITE V x d x_1

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, V' x_1 = Function.updateITE V x d x_1
Tactic:
intro v a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = Function.updateITE V x d v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = Function.updateITE V x d v
Tactic:
simp only [Function.updateITE]
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = if v = x then d else V v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = if v = x then d else V v
Tactic:
simp at a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ V' v = if v = x then d else V v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ V' v = if v = x then d else V v
Tactic:
push_neg at a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ V' v = if v = x then d else V v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
cases a1
State after:
case h.intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
left✝ : v ∉ binders
right✝ : v ≠ x
⊢ V' v = if v = x then d else V v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
case h.intro a1_left a1_right =>
  simp only [if_neg a1_right]
  exact h2 v a1_left
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (∀ (d : D),
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x d) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ∀ (a : D),
    Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ ∀ (a : D),
    Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
simp only [if_neg a1_right]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = V v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V' x = V x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = V v
Tactic:
exact h2 v a1_left
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (def_ X xs) ↔
    Holds D I V E (replace c τ (def_ X xs))
Tactic:
cases E
State after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
head✝ : Definition
tail✝ : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (head✝ :: tail✝) H
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V (head✝ :: tail✝) (replace c τ (def_ X xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))
Tactic:
case nil =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) [] H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace c τ (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) [] ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) [] ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (replace c τ (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X 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 X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X 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 X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X 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

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X 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
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp only [hd.h2]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl) ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if h : (τ X ds.length).isSome = true then
                  if ds.length = ((τ X ds.length).get ⋯).1.length then
                    Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) (hd :: tl)
                      ((τ X ds.length).get ⋯).2
                  else I.pred_var_ X ds
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V' x = V x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if h : (τ P ds.length).isSome = true then
          if ds.length = ((τ P ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V' ((τ P ds.length).get ⋯).1 ds) (hd :: tl) ((τ P ds.length).get ⋯).2
          else I.pred_var_ P ds
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
State after:
no goals