proposition: Lemma tlist_rev_app_distr {i j k} (xs : tlist B i j) (ys : tlist B j k) : tlist_rev flip (xs +++ ys) = tlist_rev flip ys +++ tlist_rev flip xs.
proof: Proof. generalize dependent i. induction xs; simpl; intros; auto. - rewrite tlist_app_tnil_l. rewrite tlist_rev_equation_1. now rewrite tlist_app_tnil_r. - rewrite <- tlist_app_comm_cons; simpl. rewrite !tlist_rev_equation_2. rewrite IHxs. now rewrite <- tlist_app_assoc. Qed.
imports: Coq.Classes.CRelationClasses Equations(Equations) Category.Lib