have := @Finset.sum_union_inter _ _ (X \ Cond) Res zlengthOf _ _
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this :
  ∑ x ∈ X \ Cond ∪ Res, zlengthOf x + ∑ x ∈ X \ Cond ∩ Res, zlengthOf x =
    ∑ x ∈ X \ Cond, zlengthOf x + ∑ x ∈ Res, zlengthOf x
⊢ zlengthOfSet (X \ Cond ∪ Res) ≤ zlengthOfSet (X \ Cond) + zlengthOfSet Res