This section (so far) contains the boolean-valued function which tests to see of two lists have the same length. This function requires both the boolean and the natural number datatypes and is separated to reduce the dependencies.
** Module lib_list_misc Imports lib_list_length lib_list_partial
same_length = ... : {s|Type}{t|Type}(list s)->(list t)->bool
Eq_length_imp_same_length_true = ... :
{t|Type}{l,m:list t}(Eq (length l) (length m))->
is_true (same_length l m)