proposition: Lemma rev'_cons : forall a (l : list A), rev' (a::l) = rev' l ++ (a::nil).
proof: Proof. intros. change (rev' ((a::nil) ++ l) = rev' l ++ (a::nil)). rewrite rev'_app. refl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)