rw [ext_iff] at h
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : var v1 = (var v2)ᶜ
⊢ False
ν : Type u_1
inst✝ : DecidableEq ν
v1 v2 : ν
h : ∀ (τ : PropAssignment ν), τ ⊨ var v1 ↔ τ ⊨ (var v2)ᶜ
⊢ False