have : zlengthOfSet Res < zlengthOfSet Cond := by
  rw [← zlen_iff]
  exact hyp
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X
X Cond Res : Finset Formula
hyp : lengthOf Res < lengthOf Cond
precondProof : Cond ⊆ X
this : zlengthOfSet Res < zlengthOfSet Cond
⊢ zlengthOfSet X - zlengthOfSet Cond + zlengthOfSet Res < zlengthOfSet X