proposition: Lemma app_eq_sub_list : forall l1 l2, l1++l2 = sub_list (l1++l2) 0 (length l1) ++ sub_list (l1++l2) (length l1) (length l2).
proof: Proof. induction l1; simpl; intros. rewrite sub_list_0, sub_list_length. refl. rewrite <- IHl1. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)