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