proposition: Lemma two_cases : forall R a m n, multiset_extension_step R n (a :: m) -> (exists n', list_permut n (a :: n') /\ multiset_extension_step R n' m) \/ (exists k, (forall b, In b k -> R b a) /\ list_permut n (k ++ m)).
proof: Proof. intros R a m n M; inversion_clear M as [x1 x2 l la a0 H H0 H1]; elim (eq_elt_dec a a0); intro a_eq_a0; subst. assert (H2 : list_permut m l). apply remove_context_list_permut_cons with a0; trivial. right; exists la; split; trivial; setoid_rewrite H0; setoid_rewrite H2; auto. left; elim (In_dec eq_elt_dec a0 m); intro In_a0. generalize (split_list_app_cons eq_elt_dec _ _ In_a0); clear In_a0; destruct (split_list eq_elt_dec m a0); intro; subst. assert (H2 : list_permut (a :: l0 ++ l1) l). apply remove_context_list_permut_cons with a0; setoid_rewrite <- H1; pattern a at 1; do 2 rewrite app_comm_cons; apply list_permut_add_cons_inside; auto. exists (la ++ l0 ++ l1); split. setoid_rewrite H0; setoid_rewrite <- H2; apply list_permut_sym; apply list_permut_add_cons_inside; auto. apply (rmv_case (l1:=la ++ l0 ++ l1) (l2:= l0 ++ a0 :: l1) (l:= l0 ++ l1) R la H); auto; apply list_permut_sym; apply list_permut_add_cons_inside; auto. absurd (In a0 (a :: m)). intro H2; elim H2; clear H2; intro H2; subst; [ absurd (a0 = a0) | absurd (In a0 m) ]; trivial. setoid_rewrite H1; left; trivial. Qed.
imports: Relations List Setoid closure more_list Multiset list_permut