proposition: Lemma netlist_concat_app {A : Type} {B : A → A → Type} {i j k} (xs : netlist (netlist B) i j) (ys : netlist (netlist B) j k) : netlist_concat (xs ++++ ys) = netlist_concat xs ++++ netlist_concat ys.
proof: Proof. induction xs; auto. rewrite <- netlist_app_comm_cons; simpl. rewrite !netlist_concat_equation_2. rewrite IHxs. now rewrite netlist_app_assoc. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib