rw [Finset.sum_sdiff_eq_sub precondProof]
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ (X \ Cond).sum zlengthOf + Res.sum zlengthOf = X.sum zlengthOf - Cond.sum zlengthOf + Res.sum zlengthOf
no goals