case pred_const_ X xs | pred_var_ X xs =>
  congr! 1
  simp only [List.map_eq_map_iff]
  exact h1
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
X : PredName
xs : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ xs, V v = V' v
⊢ I.pred_var_ X (List.map V xs) ↔ I.pred_var_ X (List.map V' xs)
no goals