proposition: Lemma context_multiset_extension_step_cons : forall R, (forall a, ~R a a) -> forall a l1 l2, multiset_extension_step R (a :: l1) (a :: l2) -> multiset_extension_step R l1 l2.
proof: Proof. intros R irrefl_R a l1 l2 H; inversion H as [a_l1 a_l2 lc lb b H' P1 P2 H2 H3]; subst. assert (a_mem_blc : mem EDS.eq_A a (b :: lc)). apply cons_permut_mem with l2 a; trivial. apply (equiv_refl _ _ eq_proof). simpl in a_mem_blc; destruct a_mem_blc as [a_eq_b | a_mem_lc]. dummy a b a_eq_b; subst b; assert (a_mem_lb_lc : mem EDS.eq_A a (lb ++ lc)). apply cons_permut_mem with l1 a; trivial. apply (equiv_refl _ _ eq_proof). rewrite <- mem_or_app in a_mem_lb_lc. destruct a_mem_lb_lc as [a_mem_lb | a_mem_lc]. absurd (R a a); [apply (irrefl_R a) | apply H'; trivial]. generalize (mem_split_set _ _ eq_bool_ok _ _ a_mem_lc). intros [a' [lc' [lc'' [a_eq_a' [H'' _]]]]]; dummy a a' a_eq_a'; subst a' lc; apply (rmv_case R (l1:=l1) (l2:= l2) (l:=lc' ++ lc'') lb (a:=a)); trivial. rewrite <- app_ass in P1; rewrite <- (permut_cons_inside) in P1. rewrite <- ass_app in P1; trivial. apply (equiv_refl _ _ eq_proof). rewrite app_comm_cons in P2; rewrite <- (permut_cons_inside) in P2; trivial. apply (equiv_refl _ _ eq_proof). generalize (mem_split_set _ _ eq_bool_ok _ _ a_mem_lc). intros [a' [lc' [lc'' [a_eq_a' [H'' _]]]]]; dummy a a' a_eq_a'; subst a' lc; apply (rmv_case R (l1:=l1) (l2:= l2) (l:=lc' ++ lc'') lb (a:=b)); trivial. rewrite <- app_ass in P1; rewrite <- (permut_cons_inside) in P1. rewrite <- ass_app in P1; trivial. apply (equiv_refl _ _ eq_proof). rewrite app_comm_cons in P2; rewrite <- (permut_cons_inside) in P2. simpl in P2; trivial. apply (equiv_refl _ _ eq_proof). Qed.
imports: Coq(Relations List Multiset Arith Morphisms FunInd) CoLoR(closure more_list list_permut ordered_set)