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

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E P zs H) V E F ↔ Holds D I V E (replace P zs H F)
Tactic:
set E_ref := E
State after:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := E
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := E
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
Tactic:
induction E generalizing F binders V
State after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
V : VarAssignment D
F : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := []
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
V : VarAssignment D
F : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := head✝ :: tail✝
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
case nil.def_ X xs =>
  simp only [replace]
  simp only [E_ref]
  simp only [Holds]
State after:
no goals

State before:
case cons
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
V : VarAssignment D
F : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := head✝ :: tail✝
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
Tactic:
induction F generalizing binders V
State after:
case cons.pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ a✝¹ a✝) ↔
    Holds D I V E_ref (replace P zs H (pred_const_ a✝¹ a✝))

case cons.pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_var_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ a✝¹ a✝) ↔ Holds D I V E_ref (replace P zs H (pred_var_ a✝¹ a✝))

case cons.eq_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ a✝¹ a✝) ↔ Holds D I V E_ref (replace P zs H (eq_ a✝¹ a✝))

case cons.true_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders true_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref true_ ↔ Holds D I V E_ref (replace P zs H true_)

case cons.false_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref (replace P zs H false_)

case cons.not_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders a✝.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref a✝.not_ ↔ Holds D I V E_ref (replace P zs H a✝.not_)

case cons.imp_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝¹ ↔ Holds D I V E_ref (replace P zs H a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (a✝¹.imp_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (a✝¹.imp_ a✝) ↔ Holds D I V E_ref (replace P zs H (a✝¹.imp_ a✝))

case cons.and_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝¹ ↔ Holds D I V E_ref (replace P zs H a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (a✝¹.and_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (a✝¹.and_ a✝) ↔ Holds D I V E_ref (replace P zs H (a✝¹.and_ a✝))

case cons.or_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝¹ ↔ Holds D I V E_ref (replace P zs H a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (a✝¹.or_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (a✝¹.or_ a✝) ↔ Holds D I V E_ref (replace P zs H (a✝¹.or_ a✝))

case cons.iff_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝¹ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝¹ ↔ Holds D I V E_ref (replace P zs H a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (a✝¹.iff_ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (a✝¹.iff_ a✝) ↔ Holds D I V E_ref (replace P zs H (a✝¹.iff_ a✝))

case cons.forall_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (forall_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (forall_ a✝¹ a✝) ↔ Holds D I V E_ref (replace P zs H (forall_ a✝¹ a✝))

case cons.exists_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders a✝ →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref a✝ ↔ Holds D I V E_ref (replace P zs H a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (exists_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ a✝¹ a✝) ↔ Holds D I V E_ref (replace P zs H (exists_ a✝¹ a✝))

case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ a✝¹ a✝)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ a✝¹ a✝) ↔ Holds D I V E_ref (replace P zs H (def_ a✝¹ a✝))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  simp only [Holds]
  simp only [I']
  simp only [Interpretation.usingPred]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (replace P zs H (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref (replace P zs H 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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H 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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (exists_ x phi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (replace P zs H (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_const_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (pred_const_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_const_ X xs) ↔ Holds D I V E_ref (pred_const_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_const_ X (List.map V xs) ↔ I.pred_const_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_const_ X (List.map V xs) ↔ I.pred_const_ X (List.map V xs)
Tactic:
simp only [I']
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_const_
      X (List.map V xs) ↔
    I.pred_const_ X (List.map V xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_const_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_const_
      X (List.map V xs) ↔
    I.pred_const_ X (List.map V xs)
Tactic:
simp only [Interpretation.usingPred]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (pred_var_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔ Holds D I V E_ref (replace P zs H (pred_var_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (pred_var_ X xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_var_ X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (I' D I V' E_ref P zs H).pred_var_ X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [I']
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_var_
      X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Interpretation.usingPred D I fun Q ds =>
          if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E_ref H
          else I.pred_var_ Q ds).pred_var_
      X (List.map V xs) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Interpretation.usingPred]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ (List.map V xs).length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ (List.map V xs).length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 :
  if X = P ∧ xs.length = zs.length then
    Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
  else True
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
split_ifs at h1
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h✝ : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h✝ : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
case neg c1 =>
  split_ifs
  case pos c2 =>
    contradiction
  case neg c2 =>
    simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admits (Function.updateListITE id zs xs) H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Sub.Var.All.Rec.admits] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H ∧ ∀ x ∈ binders, ¬(isFreeIn x H ∧ x ∉ zs)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H ∧ ∀ x ∈ binders, isFreeIn x H → x ∈ zs
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1 : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H ∧ ∀ x ∈ binders, isFreeIn x H → x ∈ zs
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
left✝ : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
right✝ : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
have s1 :
  Holds D I (V ∘ Function.updateListITE id zs xs) E_ref H ↔
    Holds D I V E_ref (Sub.Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H) :=
  by
  exact Sub.Var.All.Rec.substitution_theorem D I V E_ref (Function.updateListITE id zs xs) H h1_left
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (V ∘ Function.updateListITE id zs xs) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (V ∘ Function.updateListITE id zs xs) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [Function.updateListITE_comp] at s1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE (V ∘ id) zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE (V ∘ id) zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp at s1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
simp only [s2] at s1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
h✝ : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
case pos c2 =>
  exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
case neg _ =>
  exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
⊢ Holds D I (V ∘ Function.updateListITE id zs xs) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
exact Sub.Var.All.Rec.substitution_theorem D I V E_ref (Function.updateListITE id zs xs) H h1_left
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
⊢ ∀ (v : VarName),
    isFreeIn v H → Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
by_cases c2 : v ∈ zs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
⊢ Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ Function.updateListITE V zs (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) c2
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ zs.length = (List.map V xs).length

State before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
⊢ zs.length = (List.map V xs).length
Tactic:
cases c1
State after:
case pos.intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
left✝ : X = P
right✝ : xs.length = zs.length
⊢ zs.length = (List.map V xs).length

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = (List.map V xs).length
Tactic:
case pos.intro c1_left c1_right =>
  simp
  symm
  exact c1_right
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = (List.map V xs).length
Tactic:
simp
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = xs.length

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ zs.length = xs.length
Tactic:
symm
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ xs.length = zs.length

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∈ zs
c1_left : X = P
c1_right : xs.length = zs.length
⊢ xs.length = zs.length
Tactic:
exact c1_right
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
by_cases c3 : v ∈ binders
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
specialize h1_right v c3 a1
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
h1_right : v ∈ zs
⊢ Function.updateListITE V zs (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∈ binders
h1_right : v ∈ zs
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
contradiction
State after:
no goals

State before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ Function.updateListITE V zs (List.map V xs) v = Function.updateListITE V' zs (List.map V xs) v
Tactic:
apply Function.updateListITE_mem'
State after:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ V v = V' v

State before:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s1 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
v : VarName
a1 : isFreeIn v H
c2 : v ∉ zs
c3 : v ∉ binders
⊢ V v = V' v
Tactic:
exact h2 v c3
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = P ∧ xs.length = zs.length
h1_left : Var.All.Rec.admitsAux (Function.updateListITE id zs xs) ∅ H
h1_right : ∀ x ∈ binders, isFreeIn x H → x ∈ zs
s2 :
  Holds D I (Function.updateListITE V zs (List.map V xs)) E_ref H ↔
    Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
s1 :
  Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
exact s1
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
⊢ (if X = P ∧ xs.length = zs.length then Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E_ref
      (if X = P ∧ xs.length = zs.length then Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H
      else pred_var_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
h✝ : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
h✝ : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
case pos c2 =>
  contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)
Tactic:
case neg c2 =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : X = P ∧ xs.length = zs.length
⊢ Holds D I (Function.updateListITE V' zs (List.map V xs)) E_ref H ↔
    Holds D I V E_ref (Var.All.Rec.fastReplaceFree (Function.updateListITE id zs xs) H)
Tactic:
contradiction
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = P ∧ xs.length = zs.length)
h1 : True
c2 : ¬(X = P ∧ xs.length = zs.length)
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E_ref (pred_var_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (replace P zs H (eq_ x y))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (eq_ x y)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (eq_ x y) ↔ Holds D I V E_ref (eq_ x y)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref (replace P zs H false_)
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref false_

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref false_ ↔ Holds D I V E_ref false_
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi.not_)
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi).not_

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi.not_ ↔ Holds D I V E_ref (replace P zs H phi).not_
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ¬Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ ¬Holds D I V E_ref (replace P zs H phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ¬Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ ¬Holds D I V E_ref (replace P zs H phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)
Tactic:
exact phi_ih V binders h1 h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (phi.iff_ psi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔ Holds D I V E_ref (replace P zs H (phi.iff_ psi))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔ Holds D I V E_ref (replace P zs H (phi.iff_ psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔ Holds D I V E_ref (replace P zs H (phi.iff_ psi))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔
    Holds D I V E_ref ((replace P zs H phi).iff_ (replace P zs H psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (phi.iff_ psi) ↔
    Holds D I V E_ref ((replace P zs H phi).iff_ (replace P zs H psi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D (I' D I V' E_ref P zs H) V E_ref psi) ↔
    (Holds D I V E_ref (replace P zs H phi) ↔ Holds D I V E_ref (replace P zs H psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders phi ∧ admitsAux P zs H binders psi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D (I' D I V' E_ref P zs H) V E_ref psi) ↔
    (Holds D I V E_ref (replace P zs H phi) ↔ Holds D I V E_ref (replace P zs H psi))
Tactic:
cases h1
State after:
case intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
left✝ : admitsAux P zs H binders phi
right✝ : admitsAux P zs H binders psi
⊢ (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D (I' D I V' E_ref P zs H) V E_ref psi) ↔
    (Holds D I V E_ref (replace P zs H phi) ↔ Holds D I V E_ref (replace P zs H psi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D (I' D I V' E_ref P zs H) V E_ref psi) ↔
    (Holds D I V E_ref (replace P zs H phi) ↔ Holds D I V E_ref (replace P zs H psi))
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H 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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
phi psi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders psi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux P zs H binders phi
h1_right : admitsAux P zs H binders psi
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref psi ↔ Holds D I V E_ref (replace P zs H psi)
Tactic:
exact psi_ih V binders h1_right h2
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (exists_ x phi)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (replace P zs H (exists_ x phi))
Tactic:
simp only [admitsAux] at h1
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (replace P zs H (exists_ x phi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (replace P zs H (exists_ x phi))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (exists_ x (replace P zs H phi))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (exists_ x phi) ↔ Holds D I V E_ref (exists_ x (replace P zs H phi))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d, Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d, Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)
Tactic:
intro d
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi ↔
    Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi ↔
    Holds D I (Function.updateITE V x d) E_ref (replace P zs H 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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, Function.updateITE V x d x_1 = V' x_1

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, Function.updateITE V x d x_1 = V' x_1
Tactic:
intro v a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ Function.updateITE V x d v = V' v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ Function.updateITE V x d v = V' v
Tactic:
simp only [Function.updateITE]
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ (if v = x then d else V v) = V' v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ (if v = x then d else V v) = V' v
Tactic:
simp at a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v
Tactic:
push_neg at a1
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v

State before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
cases a1
State after:
case h.intro
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
left✝ : v ∉ binders
right✝ : v ≠ x
⊢ (if v = x then d else V v) = V' v

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = 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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∀ (d : D), Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d, Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x d) E_ref phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E_ref (replace P zs H phi)
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    Holds D (I' D I V' E_ref P zs H) (Function.updateITE V x a) E_ref phi ↔
      Holds D I (Function.updateITE V x a) E_ref (replace P zs H phi)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (binders ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
simp only [if_neg a1_right]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (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
P : PredName
zs : List VarName
H : Formula
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tail✝;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := head✝ :: tail✝
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux P zs H binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D (I' D I V' E_ref P zs H) V E_ref phi ↔ Holds D I V E_ref (replace P zs H phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H (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
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Tactic:
simp only [E_ref]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' [] P zs H) V [] (def_ X xs) ↔ Holds D I V [] (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
E_ref : Env := []
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' [] P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (replace P zs H (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref (def_ X xs) ↔ Holds D I V E_ref (def_ X xs)
Tactic:
simp only [E_ref]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' (hd :: tl) P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' (hd :: tl) P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D (I' D I V' (hd :: tl) P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      Holds D (I' D I V' (hd :: tl) P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D (I' D I V' (hd :: tl) P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) V tl (def_ X xs) ↔ Holds D I V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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:
specialize ih (Function.updateListITE V hd.args (List.map V xs)) hd.q
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) (Function.updateListITE V hd.args (List.map V xs)) E_ref hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) E_ref (replace P zs H hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) (Function.updateListITE V hd.args (List.map V xs)) E_ref hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) E_ref (replace P zs H hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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:
simp only [replace_no_predVar P zs H hd.q hd.h2] at ih
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
          Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) (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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length hd.q → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_
Tactic:
simp only [I']
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Tactic:
simp only [Interpretation.usingPred]
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length hd.q → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ hd.q.predVarSet → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ hd.q.predVarSet → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [hd.h2]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ ∅ → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : X = hd.name ∧ xs.length = hd.args.length
ih :
  ∀ (binders : Finset VarName),
    admitsAux P zs H binders hd.q →
      (∀ x ∉ binders, Function.updateListITE V hd.args (List.map V xs) x = V' x) →
        (Holds D (I' D I V' tl P zs H) (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)
⊢ ∀ (P_1 : PredName) (ds : List D),
    (P_1, ds.length) ∈ ∅ → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ Holds D (I' D I V' (hd :: tl) P zs H) 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
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length (def_ X xs) → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (I' D I V' (hd :: tl) P zs H).pred_const_ = I.pred_const_
Tactic:
simp only [I']
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ (Interpretation.usingPred D I fun Q ds =>
        if Q = P ∧ ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) (hd :: tl) H
        else I.pred_var_ Q ds).pred_const_ =
    I.pred_const_
Tactic:
simp only [Interpretation.usingPred]
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D),
    predVarOccursIn P_1 ds.length (def_ X xs) → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp only [predVarOccursIn]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D), False → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
P : PredName
zs : List VarName
H : Formula
hd : Definition
tl : List Definition
ih :
  ∀ (V : VarAssignment D) (F : Formula) (binders : Finset VarName),
    admitsAux P zs H binders F →
      (∀ x ∉ binders, V x = V' x) →
        let E_ref := tl;
        Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)
E_ref : Env := hd :: tl
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux P zs H binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P_1 : PredName) (ds : List D), False → ((I' D I V' (hd :: tl) P zs H).pred_var_ P_1 ds ↔ I.pred_var_ P_1 ds)
Tactic:
simp
State after:
no goals