proposition: Lemma context_trans_clos_multiset_extension_step_cons : forall R, transitive _ R -> (forall a, ~R a a) -> forall a l1 l2, trans_clos (multiset_extension_step R) (a :: l1) (a :: l2) -> trans_clos (multiset_extension_step R) l1 l2.
proof: Proof. intros R trans_R irrefl_R a l1 l2 H. destruct (multiset_closure trans_R H) as [ll [q [P1 [P2 [p_diff_nil [app_lt_cns cns_disj_app]]]]]]. generalize (mem_bool_ok _ _ eq_bool_ok a q). case (mem_bool DS1.eq_bool a q); [intro a_in_q | intro a_not_in_q]. destruct (mem_split_set _ _ eq_bool_ok _ _ a_in_q) as [a' [q' [q'' [a_eq_a' [H' _]]]]]; simpl in a_eq_a'; simpl in H'; subst q. rewrite ass_app in P1; rewrite <- permut_cons_inside in P1; rewrite <- ass_app in P1. rewrite ass_app in P2; rewrite <- permut_cons_inside in P2; rewrite <- ass_app in P2. apply (multiset_closure_aux R (q' ++ q'') P1 P2 p_diff_nil). intros a'' la ala'_in_ll; apply app_lt_cns; trivial. trivial. trivial. apply False_rect; apply (cns_disj_app irrefl_R a). assert (a_in_cns_ll_q : mem eq_A a (consn ll ++ q)). rewrite <- (mem_permut_mem a P2); left; trivial. apply (equiv_refl _ _ eq_proof). rewrite <- mem_or_app in a_in_cns_ll_q. destruct a_in_cns_ll_q as [a_in_cns_ll | a_in_q]; [trivial | absurd (mem eq_A a q); trivial; intro]. assert (a_in_app_ll_q : mem eq_A a (appendn ll ++ q)). rewrite <- (mem_permut_mem a P1); left; trivial. apply (equiv_refl _ _ eq_proof). rewrite <- mem_or_app in a_in_app_ll_q. destruct a_in_app_ll_q as [a_in_app_ll | a_in_q]; [trivial | absurd (mem eq_A a q); trivial]. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)