I'd like to prove for all non-empty finite sets, A and B, that: strict_subset?(A, B) => card(A) < card(B) I've searched the prelude, and extended prelude, to find several other cardinality lemmas, but not this specific one. I'm wondering whether I'm missing something, or in fact this particular lemma has yet to be shown/included. Thanks. jerome