proposition: Lemma eq_app_elim_l : forall l1 l l2, l = l1 ++ l2 -> l1 = sub_list l 0 (length l1).
proof: Proof. induction l1; destruct l; simpl; intros. refl. refl. discr. inversion H. subst. apply tail_eq. eapply IHl1. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)