fact: Parameter multiset_closure : forall R, (forall x y, {R x y}+{~R x y}) -> transitive _ R -> forall p q, trans_clos (multiset_extension_step R) p q -> exists l, exists pq, permut p ((appendn l) ++ pq) /\ permut q ((consn l) ++ pq) /\ l <> nil /\ (forall a, forall la, In (a,la) l -> forall b, mem EDS.eq_A b la -> R b a) /\ ((forall a, ~R a a) -> forall a, mem EDS.eq_A a (consn l) -> mem EDS.eq_A a (appendn l) -> False).
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)