Theorem: FOL.NV.Holds_iff_alphaEqv_Holds
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : AlphaEqv F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
induction h1 generalizing V
Proof state after:
case rename_forall_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
x✝ y✝ : VarName
a✝¹ : ¬isFreeIn y✝ phi✝
a✝ : ¬isBoundIn y✝ phi✝
V : VarAssignment D
⊢ Holds D I V E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ y✝ (Sub.Var.One.Rec.fastReplaceFree x✝ y✝ phi✝))

case rename_exists_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
x✝ y✝ : VarName
a✝¹ : ¬isFreeIn y✝ phi✝
a✝ : ¬isBoundIn y✝ phi✝
V : VarAssignment D
⊢ Holds D I V E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ y✝ (Sub.Var.One.Rec.fastReplaceFree x✝ y✝ phi✝))

case compat_not_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E phi✝.not_ ↔ Holds D I V E phi'✝.not_

case compat_imp_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.imp_ psi✝) ↔ Holds D I V E (phi'✝.imp_ psi'✝)

case compat_and_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.and_ psi✝) ↔ Holds D I V E (phi'✝.and_ psi'✝)

case compat_or_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.or_ psi✝) ↔ Holds D I V E (phi'✝.or_ psi'✝)

case compat_iff_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ psi✝ psi'✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv psi✝ psi'✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E psi✝ ↔ Holds D I V E psi'✝
V : VarAssignment D
⊢ Holds D I V E (phi✝.iff_ psi✝) ↔ Holds D I V E (phi'✝.iff_ psi'✝)

case compat_forall_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
x✝ : VarName
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E (forall_ x✝ phi✝) ↔ Holds D I V E (forall_ x✝ phi'✝)

case compat_exists_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
x✝ : VarName
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E (exists_ x✝ phi✝) ↔ Holds D I V E (exists_ x✝ phi'✝)

case refl_
D : Type
I : Interpretation D
E : Env
F F' phi✝ : Formula
V : VarAssignment D
⊢ Holds D I V E phi✝ ↔ Holds D I V E phi✝

case symm_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ : Formula
a✝ : AlphaEqv phi✝ phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
V : VarAssignment D
⊢ Holds D I V E phi'✝ ↔ Holds D I V E phi✝

case trans_
D : Type
I : Interpretation D
E : Env
F F' phi✝ phi'✝ phi''✝ : Formula
a✝¹ : AlphaEqv phi✝ phi'✝
a✝ : AlphaEqv phi'✝ phi''✝
a_ih✝¹ : ∀ (V : VarAssignment D), Holds D I V E phi✝ ↔ Holds D I V E phi'✝
a_ih✝ : ∀ (V : VarAssignment D), Holds D I V E phi'✝ ↔ Holds D I V E phi''✝
V : VarAssignment D
⊢ Holds D I V E phi✝ ↔ Holds D I V E phi''✝