case pred_ X xs =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  congr! 1
  apply List.map_congr
  intro x a1
  have s1 : ¬ x = v
  intro contra
  subst contra
  contradiction
  unfold Function.updateITE
  simp only [if_neg s1]
D : Type
I : Interpretation D
M : MetaValuation D
E : Env
Γ : List (VarName × MetaVarName)
v : VarName
h2 : ∀ (X : MetaVarName), (v, X) ∈ Γ → IsNotFree D I M E (meta_var_ X) v
X : PredName
xs : List VarName
h1 : NotFree Γ v (pred_ X xs)
⊢ IsNotFree D I M E (pred_ X xs) v
no goals