push_neg at hτ'
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 φ₂✝
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 φ₂✝