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