proposition: Lemma app_assoc : forall {A} (l l' l'' : list A), (l ++ l') ++ l'' = l ++ (l' ++ l'').
proof: Proof. intros. revert l''. funelim (l ++ l'); intros; simp app; trivial. now rewrite H. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat