rw [this, this]
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ zlengthOfSet X < zlengthOfSet Y
X Y : Finset Formula
this : ∀ (W : Finset Formula), zlengthOfSet W = ↑(lengthOfSet W)
⊢ lengthOf X < lengthOf Y ↔ ↑(lengthOfSet X) < ↑(lengthOfSet Y)