proposition: Lemma split_aux_correct : forall l n l1 l2 acc, split_aux acc l n = Some (l1, l2) -> rev' acc ++ l = l1 ++ l2.
proof: Proof. induction l; destruct n; simpl; intros. inversion H. refl. discr. inversion H. refl. ded (IHl _ _ _ _ H). rewrite rev'_cons in H0. rewrite app_ass in H0. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)