proposition: Lemma netlist_app_comm_cons {i j k l} (x : B i j) (xs : netlist B j k) (ys : netlist B k l) : x :::: (xs ++++ ys) = (x :::: xs) ++++ ys.
proof: Proof. now rewrite netlist_app_equation_2. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib