proposition: Lemma tlist_app_assoc {i j k l} (xs : tlist B i j) (ys : tlist B j k) (zs : tlist B k l) : (xs +++ ys) +++ zs = xs +++ (ys +++ zs).
proof: Proof. induction xs; auto. now rewrite <- !tlist_app_comm_cons, IHxs. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib