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