induction φ generalizing τ with
| tr => exfalso; exact hτ' satisfies_tr
| fls => exfalso; exact not_satisfies_fls hτ
| var y =>
  simp_all only [vars, satisfies_var, Finset.mem_singleton]
  by_contra h
  exact hτ' (hτ ▸ τ.set_get_of_ne (!τ x) h)
| _ =>
  simp_all only
    [satisfies_conj, satisfies_disj, satisfies_impl', satisfies_biImpl', vars, Finset.mem_union]
  push_neg at hτ'
  aesop
ν : Type u_1
inst✝ : DecidableEq ν
φ : PropForm ν
τ : PropAssignment ν
x : ν
hτ : τ ⊨ φ
hτ' : ¬(PropAssignment.set τ x !τ x) ⊨ φ
⊢ x ∈ vars φ
no goals