simp only [predVarOccursIn]
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ predVarOccursIn P n (def_ a✝¹ a✝) ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet
case def_
P : PredName
n : ℕ
a✝¹ : DefName
a✝ : List VarName
⊢ False ↔ (P, n) ∈ (def_ a✝¹ a✝).predVarSet