exact isAlphaEqv_Holds_aux D I V V E F F' [] AlphaEqvVarAssignment.nil h1
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'
no goals