case pred_ X xs =>
  unfold NoMetaVarAndAllFreeInList at h1
  unfold NotFree
  tauto
v : VarName
Γ : List (VarName × MetaVarName)
X : PredName
xs vs : List VarName
h1 : NoMetaVarAndAllFreeInList vs (pred_ X xs)
h2 : v ∉ vs
⊢ NotFree Γ v (pred_ X xs)
no goals