proposition: Lemma append_assoc {f g h} : append f (append g h) = append (append f g) h.
proof: Proof. induction f; simpl; auto. now rewrite IHf. Qed.
imports: Coq.Lists.List Equations(Equations) Category.Lib Category.Theory.Category Category.Solver.Expr Category.Solver.Denote Category.Solver.Reify