proposition: Lemma rev_app' : forall {A} (l l' : list A), rev (l +++ l') = rev l' +++ rev l.
proof: Proof. intros. funelim (l +++ l'); simp rev app'; trivial. now (rewrite H, <- app'_assoc). Qed.
imports: Program Bvector List Relations Equations.Prop.Equations Utf8 Arith Wf_nat Vectors.Vector