linarith
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
no goals