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