simp
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∪ {x}
v x : VarName
phi : Formula
phi_ih : isBoundIn v phi ↔ v ∈ phi.boundVarSet
⊢ v = x ∨ isBoundIn v phi ↔ v ∈ phi.boundVarSet ∨ v = x