proposition: Lemma nil_is_the_smallest : forall R e l, trans_clos (multiset_extension_step R) nil (e :: l).
proof: Proof. intros R e' l; generalize e'; clear e'; induction l as [ | e l]. intros e; apply t_step; refine (@rmv_case _ _ _ nil nil e _ _ _); auto; contradiction. intros e'; apply trans_clos_is_trans with (e' :: l); trivial. apply t_step; refine (@rmv_case _ _ _ (e' :: l) nil e _ _ _); auto. contradiction. rewrite <- (permut_cons_inside (e1 := e') (e2 := e') (e :: l) (e :: nil) l). auto. apply (equiv_refl _ _ eq_proof). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)