proposition: Lemma tlist_rev_unit {i j k} (xs : tlist B i j) (x : B j k) : tlist_rev flip (xs +++ x ::: tnil) = flip _ _ x ::: tlist_rev flip xs.
proof: Proof. induction xs; auto; simpl. rewrite <- tlist_app_comm_cons; simpl. rewrite tlist_rev_equation_2. now rewrite IHxs. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib