fact: Fixpoint tlist_concat {i j} (xs : tlist (tlist B) i j) : tlist B i j := match xs with | tnil => tnil | tcons _ x xs => x +++ tlist_concat xs end.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib