proposition: Lemma netlist_concat_tadd {i j k} (x : netlist B i j) (xs : netlist (netlist B) j k) : netlist_concat (x :::: xs) = x ++++ netlist_concat xs.
proof: Proof. reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib