proposition: Lemma tlist_app_length {i j k} (xs : tlist B i j) (ys : tlist B j k) : tlist_length (xs +++ ys) = (tlist_length xs + tlist_length ys)%nat.
proof: Proof. induction xs; auto. rewrite <- tlist_app_comm_cons; simpl. now rewrite IHxs. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib