set E_ref := E
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D (I' D I V' E P zs H) V E F ↔ Holds D I V E (replace P zs H F)
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F : Formula
P : PredName
zs : List VarName
H : Formula
binders : Finset VarName
h1 : admitsAux P zs H binders F
h2 : ∀ x ∉ binders, V x = V' x
E_ref : Env := E
⊢ Holds D (I' D I V' E_ref P zs H) V E_ref F ↔ Holds D I V E_ref (replace P zs H F)