simp only [zlengthOfSet]
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond) + zlengthOfSet Res = zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res
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