proposition: Lemma permut_inv_right_strong : forall (A B : Type) (R : A -> B -> Prop) b l1 l2' l2'', permut0 R l1 (l2' ++ b :: l2'') -> exists a, exists l1', exists l1'', (R a b /\ l1 = l1' ++ a :: l1'' /\ permut0 R (l1' ++ l1'') (l2' ++ l2'')).
proof: Proof. intros A B R b l1; generalize b; clear b; induction l1 as [ | a1 l1]; intros b l2' l2'' P; inversion P as [ | a b' l' l1' k2 a_R_b' Q H]; subst. destruct l2'; discriminate. destruct (in_in_split_set _ _ _ _ _ _ H1) as [[H2' | H2'] | H2']; clear H1. destruct H2' as [l [H2 H3]]; subst. rewrite <- ass_app in Q; simpl in Q; destruct (IHl1 b _ _ Q) as [a [l1' [l1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: l1'); exists l1''; repeat split; trivial. simpl; rewrite ass_app; apply Pcons; trivial. rewrite <- ass_app; trivial. destruct H2' as [l [H2 H3]]; subst. rewrite ass_app in Q. destruct (IHl1 b _ _ Q) as [a [k1' [k1'' [a_R_b [H Q']]]]]; subst. exists a; exists (a1 :: k1'); exists k1''; repeat split; trivial. rewrite <- ass_app; simpl; apply Pcons; trivial. rewrite ass_app; trivial. destruct H2' as [b'_eq_b [H2 H3]]; subst. exists a1; exists (@nil A); exists l1; repeat split; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)