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