proposition: Lemma two_cases : forall R a m n, multiset_extension_step R n (a :: m) -> (exists n', permut n (a :: n') /\ multiset_extension_step R n' m) \/ (exists k, (forall b, mem EDS.eq_A b k -> R b a) /\ permut n (k ++ m)).
proof: Proof. intros R a m n M; inversion_clear M as [x1 x2 l la b H H0 H1]; generalize (eq_bool_ok a b); case (DS1.eq_bool a b); [intro a_eq_b; subst b | intro a_diff_b]. rewrite <- permut_cons in H1; [idtac | apply (equiv_refl _ _ eq_proof)]. right; exists la; split; trivial. apply permut_trans with (la ++ l). assumption. rewrite <- permut_app1; auto. left; generalize (remove_is_sound b m); case (@remove A eq_bool b m). intros m' P; exists (la ++ m'); split. refine (permut_trans H0 _). apply permut_trans with (la ++ a :: m'). refine (proj1 (permut_app1 _ _ _) _). apply permut_sym. rewrite (@permut_cons b b (a :: m') l). apply permut_trans with (a :: m). apply permut_sym; rewrite <- (permut_cons_inside (e1 := a) (e2 := a) m (b :: nil) m'). assumption. apply (equiv_refl _ _ eq_proof). assumption. apply (equiv_refl _ _ eq_proof). apply permut_sym; rewrite <- (permut_cons_inside (e1 := a) (e2 := a) (la ++ m') la m'). apply permut_refl. apply (equiv_refl _ _ eq_proof). apply (rmv_case (l1:=la ++ m') (l2:= m) (l:= m') R la H); auto; apply permut_sym; rewrite <- permut_cons_inside; auto. intro b_not_mem_m; apply False_rect. assert (b_mem_am : mem EDS.eq_A b (a :: m)). rewrite (mem_permut_mem b H1); left. apply (equiv_refl _ _ eq_proof). simpl in b_mem_am; case b_mem_am; clear b_mem_am. intro; apply a_diff_b; apply sym_eq; assumption. exact b_not_mem_m. Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)