proposition: Lemma tlist_concat_app {A : Type} {B : A → A → Type} {i j k} (xs : tlist (tlist B) i j) (ys : tlist (tlist B) j k) : tlist_concat (xs +++ ys) = tlist_concat xs +++ tlist_concat ys.
proof: Proof. induction xs; auto. rewrite <- tlist_app_comm_cons; simpl. rewrite IHxs. now rewrite tlist_app_assoc. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib