proposition: Lemma ac_syntactic : forall (l1 l2 l3 l4 : list A), permut (l2 ++ l1) (l4 ++ l3) -> (exists u1, exists u2, exists u3, exists u4, permut l1 (u1 ++ u2) /\ permut l2 (u3 ++ u4) /\ permut l3 (u1 ++ u3) /\ permut l4 (u2 ++ u4)).
proof: Proof. intros l1 l2 l3 l4 P; apply ac_syntactic_aux. apply permut_trans with (l2 ++ l1). apply list_permut_app_app. apply permut_trans with (l4 ++ l3); trivial. apply list_permut_app_app. Qed.
imports: Coq(List Relations Arith Setoid Morphisms FunInd) CoLoR(decidable_set more_list equiv_list)