cases hv
case biImpl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
hv :
  v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v') ∨
    v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ
case biImpl.inl
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₁ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ

case biImpl.inr
ν : Type u_1
inst✝ : DecidableEq ν
φ φ₁✝ φ₂✝ : PropForm ν
v✝ : ν
ψ ψ₁ ψ₂ φ₁ φ₂ : PropForm ν
ih₁ : vars (substOne φ₁ v✝ ψ) ⊆ vars φ₁ \ {v✝} ∪ vars ψ
ih₂ : vars (substOne φ₂ v✝ ψ) ⊆ vars φ₂ \ {v✝} ∪ vars ψ
v : ν
h✝ : v ∈ vars (subst φ₂ fun v' => if v' = v✝ then ψ else var v')
⊢ (v ∈ vars φ₁ ∨ v ∈ vars φ₂) ∧ ¬v = v✝ ∨ v ∈ vars ψ