proposition: Lemma app_nil : forall {A} (l : list A), l ++ [] = l.
proof: Proof. intros. funelim (app l []); simpl. reflexivity. now rewrite H. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat