case eq_ x y =>
  unfold NotFree at h1
  unfold IsNotFree
  simp only [Holds]
  intro V d
  cases h1
  case intro h1_left h1_right =>
    simp only [Function.updateITE]
    simp only [if_neg h1_left]
    simp only [if_neg h1_right]
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 y : VarName
h1 : NotFree Γ v (eq_ x y)
⊢ IsNotFree D I M E (eq_ x y) v
no goals