proposition: Lemma tlist_rev_involutive {i j} (xs : tlist B i j) : tlist_rev flip (tlist_rev flip xs) = xs.
proof: Proof. Proof using A B flip flip_involutive. induction xs; simpl; auto. rewrite tlist_rev_equation_2. rewrite tlist_rev_app_distr. rewrite IHxs. rewrite tlist_rev_equation_2. rewrite tlist_rev_equation_1. rewrite flip_involutive. rewrite tlist_app_equation_1. now rewrite <- tlist_app_cons. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib