proposition: Lemma tlist_concat_tcons {i j k} (x : tlist B i j) (xs : tlist (tlist B) j k) : tlist_concat (x ::: xs) = x +++ tlist_concat xs.
proof: Proof. reflexivity. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib