fact: Definition eq_bool al1 al2 : bool := match al1, al2 with | (e1,l1), (e2,l2) => if DS1.eq_bool e1 e2 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)