have := h (fun v => v = v1 || v = v2)
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
⊢ False
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ (var v1)ᶜ ↔ τ ⊨ var v2
this :
  (fun v => decide (v = v1) || decide (v = v2)) ⊨ (var v1)ᶜ ↔ (fun v => decide (v = v1) || decide (v = v2)) ⊨ var v2
⊢ False