proposition: Lemma rev_rev_acc : forall {A} (l : list A), rev_acc l [] = rev l.
proof: Proof. intros. replace (rev l) with (rev l ++ []) by apply app_nil. generalize (@nil A). funelim (rev l). reflexivity. intros l'. simp rev_acc; trivial. rewrite H. rewrite app_assoc. reflexivity. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat