fact: Fixpoint eq_bool_list l1 l2: bool := match l1, l2 with | nil, nil => true | nil, (_ :: _) => false | (a1 :: l1), nil => false | (a1 :: l1), (a2 :: l2) => if DS1.eq_bool a1 a2 then eq_bool_list l1 l2 else false end.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)