simp only [Finset.mem_biUnion, Finset.mem_union]
case a.h.e'_1.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ phi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ phi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ)
case a.h.e'_1.a.h2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
x : VarName
a1 : ∃ a ∈ phi.predVarSet, x ∈ predVarFreeVarSet τ a
a : PredName × ℕ
a2 : a ∈ phi.predVarSet ∧ x ∈ predVarFreeVarSet τ a
⊢ ∃ a, (a ∈ phi.predVarSet ∨ a ∈ psi.predVarSet) ∧ x ∈ predVarFreeVarSet τ a