proposition: Lemma rev_app : forall l1 l2, rev (l1 ++ l2) = rev l2 ++ rev l1.
proof: Proof. Proof using. intros. unfold rev. asserts K1: (forall l accu, fold_left (fun x acc => x :: acc) accu l = fold_left (fun x acc => x :: acc) nil l ++ accu). { induction l; intros. { auto. } { rew_listx. rewrite IHl. rewrite (@IHl (a::nil)). rew_list~. } } asserts K2: (forall accu, fold_left (fun x acc => x :: acc) accu (l1 ++ l2) = fold_left (fun x acc => x :: acc) nil l2 ++ fold_left (fun x acc => x :: acc) nil l1 ++ accu). { induction l1; intros. { rew_list. apply K1. } { rew_listx. rewrite IHl1. rewrite (@K1 l1 (a::nil)). rew_list~. } } lets K3: (@K2 nil). rewrite app_nil_r in K3. auto. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)