proposition: Lemma netlist_app_assoc {i j k l} (xs : netlist B i j) (ys : netlist B j k) (zs : netlist B k l) : (xs ++++ ys) ++++ zs = xs ++++ (ys ++++ zs).
proof: Proof. induction xs; auto. now rewrite <- !netlist_app_comm_cons, IHxs. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib