intro v 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 ψ
⊢ vars (substOne (biImpl φ₁ φ₂) v ψ) ⊆ vars (biImpl φ₁ φ₂) \ {v} ∪ vars ψ
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 (substOne (biImpl φ₁ φ₂) v✝ ψ)
⊢ v ∈ vars (biImpl φ₁ φ₂) \ {v✝} ∪ vars ψ