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(Equations Signature) Utf8 Arith Wf_nat