apply h2
case neg
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ V'' x = V x
case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∈ H.freeVarSet

case neg.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
c1 : (τ X xs.length).isSome = true
zs : List VarName := ((τ X xs.length).get ⋯).1
c2 : xs.length = zs.length
H : Formula := ((τ X xs.length).get ⋯).2
h2 : ∀ x ∈ H.freeVarSet, x ∉ zs → V'' x = V x
x : VarName
a1 : isFreeIn x H
c3 : x ∉ zs
⊢ x ∉ zs