proposition: Lemma permut_strong : forall (A B : Type) (R : A -> B -> Prop) a1 a2 l1 k1 l2 k2, R a1 a2 -> permut0 R (l1 ++ k1) (l2 ++ k2) -> permut0 R (l1 ++ a1 :: k1) (l2 ++ a2 :: k2).
proof: Proof. intros A B R a1 a2 l1; induction l1 as [ | u1 l1]; intros k1 l2 k2 a1_R_a2 P. apply (@Pcons _ _ R a1 a2 k1 l2 k2); trivial. inversion P as [ | b1 b2 l k k' b1_R_b2 Q]; clear P; subst. destruct (split_list _ _ _ _ H1) as [H' | H']; clear H1. destruct H' as [l [H1 H2]]; subst; simpl. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (l2 ++ a2 :: l) k' b1_R_b2). do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'. apply IHl1; trivial. rewrite ass_app; trivial. destruct H' as [l [H1 H2]]; subst; simpl. destruct l as [ | u l]. simpl in H2; subst k2; rewrite <- app_nil_end. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) (k ++ a2 :: nil) k' b1_R_b2). do 2 rewrite <- ass_app in Q'; simpl in Q'; apply Q'. apply IHl1; trivial. simpl in H2; injection H2; clear H2; intros H2 b2_eq_u; subst u k'. assert (Q' := @Pcons _ _ R u1 b2 (l1 ++ a1 :: k1) k (l ++ a2 :: k2) b1_R_b2). rewrite <- ass_app; simpl; apply Q'. rewrite ass_app; apply IHl1; trivial. rewrite <- ass_app; trivial. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)