contradiction
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : ¬x = x
⊢ V' t = V x
no goals