proposition: Lemma sub_list_length : forall l, sub_list l 0 (length l) = l.
proof: Proof. induction l; simpl; intros. refl. rewrite IHl. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)