proposition: Lemma rev'_app : forall l l' : list A, rev' (l ++ l') = rev' l' ++ rev' l.
proof: Proof. intros. rewrite rev_append_app, !rev_append_rev, <- !app_nil_end. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)