case intro h1_left h1_right =>
  congr! 1
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 y : VarName
V V' : VarAssignment D
h1_left : V x = V' x
h1_right : V y = V' y
⊢ V x = V y ↔ V' x = V' y
no goals