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. rewrite H. rewrite app'_assoc. reflexivity. Qed.
imports: Program Bvector List Relations Equations.Prop.Equations Utf8 Arith Wf_nat Vectors.Vector