proposition: Lemma multiset_closure_aux : forall (R : relation A) p q l 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) -> trans_clos (multiset_extension_step R) p q.
proof: Proof. intros R p q l; generalize p q; clear p q; induction l as [ | [x lx] l]. simpl; intros p q pq Pp Pq H; absurd (@nil (A * list A) = nil); trivial. simpl; intros p q pq Pp Pq _ H. assert (lx_lt_x : forall b, mem EDS.eq_A b lx -> R b x). apply H; left; trivial. destruct l as [ | [y ly] l]; simpl in *. rewrite <- app_nil_end in Pp. simpl in Pq; apply t_step. exact (rmv_case R lx lx_lt_x Pp Pq). apply t_trans with (x :: ly ++ (appendn l) ++ pq). do 2 rewrite app_ass in Pp; refine (rmv_case R lx lx_lt_x Pp (permut_refl _)). refine (list_permut_trans_clos_multiset_extension_step_2 (permut_sym Pq) _). apply (@context_trans_clos_multiset_extension_step_app1 R (ly ++ appendn l ++ pq) (y :: consn l ++ pq) (x :: nil)); apply (@IHl (ly ++ appendn l ++ pq) (y :: consn l ++ pq) pq); auto. rewrite ass_app; auto. discriminate. intros a la H1 b b_in_la; apply (H a la); trivial; right; trivial. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)