proposition: Lemma netlist_app_length {i j k} (xs : netlist B i j) (ys : netlist B j k) : netlist_length (xs ++++ ys) = (netlist_length xs + netlist_length ys)%nat.
proof: Proof. induction xs; auto. rewrite <- netlist_app_comm_cons; simpl. now rewrite IHxs. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib