simp_all only
  [satisfies_conj, satisfies_disj, satisfies_impl', satisfies_biImpl', vars, Finset.mem_union]
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ biImpl φ₁✝ φ₂✝
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ biImpl φ₁✝ φ₂✝
⊢ x ∈ vars (biImpl φ₁✝ φ₂✝)
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
x : ν
φ₁✝ φ₂✝ : PropForm ν
φ₁_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₁✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ → x ∈ vars φ₁✝
φ₂_ih✝ : ∀ {τ : PropAssignment ν}, τ ⊨ φ₂✝ → ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝ → x ∈ vars φ₂✝
τ : PropAssignment ν
hτ : τ ⊨ φ₁✝ ∧ τ ⊨ φ₂✝ ∨ ¬τ ⊨ φ₁✝ ∧ ¬τ ⊨ φ₂✝
hτ' :
  ¬((PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ (PropAssignment.set τ x !τ x) ⊨ φ₂✝ ∨
      ¬(PropAssignment.set τ x !τ x) ⊨ φ₁✝ ∧ ¬(PropAssignment.set τ x !τ x) ⊨ φ₂✝)
⊢ x ∈ vars φ₁✝ ∨ x ∈ vars φ₂✝