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

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqv F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
simp only [isAlphaEqv] at h1
State after:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqvAux [] F F'
⊢ Holds D I V E F ↔ Holds D I V E F'

State before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
F F' : Formula
h1 : isAlphaEqvAux [] F F'
⊢ Holds D I V E F ↔ Holds D I V E F'
Tactic:
exact isAlphaEqv_Holds_aux D I V V E F F' [] AlphaEqvVarAssignment.nil h1
State after:
no goals