proposition: Lemma tlist_app_comm_cons {i j k l} (x : B i j) (xs : tlist B j k) (ys : tlist B k l) : x ::: (xs +++ ys) = (x ::: xs) +++ ys.
proof: Proof. now destruct xs, ys. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib