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