proposition: Lemma tlist_rev_length {i j} (xs : tlist B i j) : tlist_length (tlist_rev flip xs) = tlist_length xs.
proof: Proof. induction xs; auto; simpl. rewrite tlist_rev_equation_2. rewrite tlist_app_length, IHxs; simpl. apply PeanoNat.Nat.add_1_r. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib