rw [zlen_iff]
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ lengthOf (X \ Cond ∪ Res) < lengthOf X
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet (X \ Cond ∪ Res) < zlengthOfSet X