apply substitution_theorem_aux
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ Holds D (I' D I V E τ) V E F ↔ Holds D I V E (sub c τ F)
case h1
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ (x : VarName), isFreeIn x F → V x = V (id x)

case h2
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
F : Formula
⊢ ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V x = V x