by_cases c1 : x = v
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
⊢ x = v ∨ NotFree Γ v phi
case pos
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : x = v
⊢ x = v ∨ NotFree Γ v phi

case neg
v : VarName
Γ : List (VarName × MetaVarName)
x : VarName
phi : Formula
phi_ih : ∀ (vs : List VarName), NoMetaVarAndAllFreeInList vs phi → v ∉ vs → NotFree Γ v phi
vs : List VarName
h2 : v ∉ vs
h1 : NoMetaVarAndAllFreeInList (x :: vs) phi
c1 : ¬x = v
⊢ x = v ∨ NotFree Γ v phi