case true_ | false_ =>
  simp only [subAux]
  simp only [Holds]
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E (subAux c τ σ false_)
no goals