proposition: Lemma multiset_closure_aux2 : forall (R : relation A) p q le l pq, permut p ((appendn l) ++ pq) -> permut q (le ++ (consn l) ++ pq) -> l <> nil \/ le <> 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 le l pq Pp Pq H H'; apply (@multiset_closure_aux R p q ((map (fun x => (x, @nil A)) le) ++ l) pq). apply permut_trans with (appendn l ++ pq). assumption. rewrite <- permut_app2; rewrite appendn_app; clear Pq H; induction le as [ | e le]; simpl; auto. apply permut_trans with (le ++ consn l ++ pq). assumption. rewrite ass_app; rewrite <- permut_app2; rewrite consn_app; clear Pq H; induction le as [ | e le]; simpl; auto. rewrite <- permut_cons; trivial. apply (equiv_refl _ _ eq_proof). intro H''; destruct (app_eq_nil _ _ H'') as [ l_eq_nil le_eq_nil]; destruct H as [le_diff_nil | l_diff_nil]. absurd (l = nil); trivial. destruct le as [ | e le]. absurd (@nil A = nil); trivial. discriminate. clear Pq H; induction le as [ | e le]; simpl; trivial. intros a la [H | H] b b_in_la; [injection H; intros; subst; contradiction | apply (IHle a la); trivial]. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)