kernel_objects.pl

card_leq(Set,Card) :-
    ((nonvar(Set),is_custom_explicit_set(Set,card_leq))
    -> explicit_set_cardinality(Set,CCard), leq_int_peano(CCard,Card)
    ; card_leq2(Set,Card) ).

card_leq2([],_C).

card_leq2([_|T],s(C)) :- card_leq2(T,C). %when(nonvar(T),card_leq2(T,C)).

card_leq2(avl_set(A),C) :- card_leq(avl_set(A),C).

card_leq2(closure(P,T,B),C) :- card_leq(closure(P,T,B),C).

card_leq2(global_set(A),C) :- card_leq(global_set(A),C).

card_leq2(freetype(A),C) :- card_leq(freetype(A),C).

leq_int_peano(0,_).

leq_int_peano(inf,_) :- !,fail.

leq_int_peano(X,s(C)) :- X>0, X1 is X-1, leq_int_peano(X1,C).