Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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:
cases F'
Proof state after:
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✝)