simp
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
psi_ih : occursIn v psi ∧ v.isBound ↔ v ∈ psi.boundVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isBound ↔ v ∈ phi.boundVarSet ∪ psi.boundVarSet
v : Var
phi psi : Formula
phi_ih : occursIn v phi ∧ v.isBound ↔ v ∈ phi.boundVarSet
psi_ih : occursIn v psi ∧ v.isBound ↔ v ∈ psi.boundVarSet
⊢ (occursIn v phi ∨ occursIn v psi) ∧ v.isBound ↔ v ∈ phi.boundVarSet ∨ v ∈ psi.boundVarSet