proposition: Lemma permut_add_inside : forall (A B : Type) (R : A -> B -> Prop) a b l1 l1' l2 l2', (forall a1 b1 a2 b2, In a1 (l1 ++ a :: l1') -> In b1 (l2 ++ b :: l2') -> In a2 (l1 ++ a :: l1') -> In b2 (l2 ++ b :: l2') -> R a1 b1 -> R a2 b1 -> R a2 b2 -> R a1 b2) -> R a b -> permut0 R (l1 ++ a :: l1') (l2 ++ b :: l2') -> permut0 R (l1 ++ l1') (l2 ++ l2').
proof: Proof. intros A B R a b l1 l1' l2 l2' trans_R a_R_b P. destruct (permut_inv_left_strong (R := R) _ _ _ P) as [b' [k2 [k2' [a_R_b' [H P']]]]]. destruct (in_in_split_set _ _ _ _ _ _ H) as [[H' | H'] | H']; clear H. destruct H' as [l [H1 H2]]; subst. rewrite ass_app in P'. destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]]. rewrite H; rewrite <- ass_app; simpl; apply permut_strong. apply trans_R with b a; trivial. apply in_insert; rewrite H; apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; left; apply in_or_app; right; left; trivial. rewrite ass_app; trivial. destruct H' as [l [H1 H2]]; subst. rewrite <- ass_app in P'; simpl in P'. destruct (permut_inv_right_strong (R := R) _ _ _ P') as [a' [k1' [k1'' [a'_R_b' [H P'']]]]]. rewrite H; rewrite ass_app; simpl; apply permut_strong. apply trans_R with b a; trivial. apply in_insert; rewrite H; apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; left; trivial. apply in_or_app; right; right; apply in_or_app; right; left; trivial. rewrite <- ass_app; trivial. destruct H' as [H1 [H2 H3]]; subst; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)