Theorem: FOL.NV.isAlphaEqv_Holds_aux (FOL/NV/Alpha.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V E F ↔ Holds D I V' E F'
Tactic:
induction E generalizing F F' binders V V'
State after:
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V [] F ↔ Holds D I V' [] F'

case cons
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) F'

State before:
D : Type
I : Interpretation D
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : a✝³ = a✝¹ ∧ isAlphaEqvVarList binders a✝² a✝
⊢ Holds D I V [] (def_ a✝³ a✝²) ↔ Holds D I V' [] (def_ a✝¹ a✝)
Tactic:
case nil.def_.def_ =>
  simp only [Holds]
State after:
no goals

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

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

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

case cons.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders true_ F'
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) F'

case cons.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders false_ F'
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) F'

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

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

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

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

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

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

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

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

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

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

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

case cons.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders true_ F'
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) F'

case cons.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders false_ F'
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) F'

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

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

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

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

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

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

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

case cons.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (def_ a✝¹ a✝) F'
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) F'
Tactic:
all_goals
  cases F'
State after:
case cons.pred_const_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.pred_const_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.pred_const_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.pred_const_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (pred_const_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.pred_const_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (pred_const_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.pred_const_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : PredName
a✝¹ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.pred_const_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.pred_const_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.pred_const_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.pred_const_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.pred_const_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.pred_const_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.pred_const_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_const_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_const_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.pred_var_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.pred_var_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.pred_var_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.pred_var_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (pred_var_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.pred_var_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (pred_var_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.pred_var_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : PredName
a✝¹ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.pred_var_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.pred_var_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.pred_var_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.pred_var_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.pred_var_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.pred_var_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.pred_var_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : PredName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (pred_var_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (pred_var_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.eq_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.eq_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.eq_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.eq_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (eq_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.eq_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (eq_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.eq_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² a✝¹ : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.eq_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.eq_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.eq_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.eq_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.eq_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.eq_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.eq_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (eq_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (eq_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.true_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders true_ (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.true_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders true_ (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.true_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders true_ (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.true_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders true_ true_
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.true_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders true_ false_
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.true_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders true_ a✝.not_
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.true_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders true_ (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.true_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders true_ (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.true_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders true_ (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.true_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders true_ (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.true_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders true_ (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.true_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders true_ (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.true_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders true_ (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) true_ ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.false_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders false_ (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.false_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders false_ (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.false_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders false_ (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.false_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders false_ true_
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.false_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders false_ false_
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.false_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders false_ a✝.not_
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.false_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders false_ (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.false_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders false_ (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.false_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders false_ (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.false_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders false_ (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.false_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders false_ (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.false_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders false_ (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.false_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders false_ (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) false_ ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.not_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders a✝².not_ (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.not_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders a✝².not_ (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.not_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders a✝².not_ (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.not_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders a✝.not_ true_
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.not_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders a✝.not_ false_
⊢ Holds D I V (head✝ :: tail✝) a✝.not_ ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.not_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders a✝¹.not_ a✝.not_
⊢ Holds D I V (head✝ :: tail✝) a✝¹.not_ ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.not_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.not_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.not_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.not_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.not_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.not_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders a✝².not_ (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.not_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders a✝².not_ (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) a✝².not_ ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.imp_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.imp_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.imp_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.imp_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.imp_ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.imp_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.imp_ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.imp_ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.imp_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² a✝¹ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝².imp_ a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (a✝².imp_ a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.imp_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.imp_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.imp_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.imp_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.imp_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.imp_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.imp_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.imp_ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.imp_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.and_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.and_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.and_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.and_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.and_ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.and_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.and_ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.and_ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.and_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² a✝¹ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝².and_ a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (a✝².and_ a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.and_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.and_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.and_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.and_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.and_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.and_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.and_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.and_ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.and_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.or_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.or_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.or_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.or_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.or_ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.or_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.or_ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.or_ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.or_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² a✝¹ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝².or_ a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (a✝².or_ a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.or_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.or_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.or_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.or_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.or_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.or_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.or_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.or_ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.or_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.iff_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.iff_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.iff_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.iff_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.iff_ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.iff_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (a✝¹.iff_ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (a✝¹.iff_ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.iff_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² a✝¹ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝².iff_ a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (a✝².iff_ a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.iff_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.iff_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.iff_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.iff_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.iff_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.iff_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.iff_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ a✝² : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝³ F' → (Holds D I V (head✝ :: tail✝) a✝³ ↔ Holds D I V' (head✝ :: tail✝) F')
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (a✝³.iff_ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (a✝³.iff_ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.forall_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.forall_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.forall_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.forall_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (forall_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.forall_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (forall_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.forall_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : VarName
a✝¹ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.forall_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.forall_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.forall_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.forall_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.forall_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.forall_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.forall_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (forall_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (forall_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.exists_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.exists_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.exists_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.exists_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (exists_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.exists_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝ F' → (Holds D I V (head✝ :: tail✝) a✝ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (exists_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.exists_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : VarName
a✝¹ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝¹ F' → (Holds D I V (head✝ :: tail✝) a✝¹ ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.exists_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.exists_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.exists_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.exists_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.exists_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.exists_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.exists_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : VarName
a✝² : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders a✝² F' → (Holds D I V (head✝ :: tail✝) a✝² ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (exists_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (exists_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)

case cons.def_.pred_const_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (pred_const_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_const_ a✝¹ a✝)

case cons.def_.pred_var_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : PredName
a✝ : List VarName
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (pred_var_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (pred_var_ a✝¹ a✝)

case cons.def_.eq_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : VarName
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (eq_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (eq_ a✝¹ a✝)

case cons.def_.true_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (def_ a✝¹ a✝) true_
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) true_

case cons.def_.false_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders (def_ a✝¹ a✝) false_
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) false_

case cons.def_.not_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝² : DefName
a✝¹ : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝² a✝¹) a✝.not_
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝² a✝¹) ↔ Holds D I V' (head✝ :: tail✝) a✝.not_

case cons.def_.imp_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (a✝¹.imp_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.imp_ a✝)

case cons.def_.and_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (a✝¹.and_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.and_ a✝)

case cons.def_.or_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (a✝¹.or_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.or_ a✝)

case cons.def_.iff_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (a✝¹.iff_ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (a✝¹.iff_ a✝)

case cons.def_.forall_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (forall_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (forall_ a✝¹ a✝)

case cons.def_.exists_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : VarName
a✝ : Formula
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (exists_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (exists_ a✝¹ a✝)

case cons.def_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)