proposition: Lemma app_assoc {A} (x y z : list A) : x ++ y ++ z = (x ++ y) ++ z.
proof: Proof. induction x; simpl; auto. now rewrite IHx. Defined.
imports: Program.Basics Program.Tactics Equations.Equations Coq.Vectors.VectorDef List Equations(Fin)