proposition: Lemma netlist_rev_length {i j} (xs : netlist B i j) : netlist_length (netlist_rev flip xs) = netlist_length xs.
proof: Proof. induction xs; auto; simpl. rewrite netlist_rev_equation_2. rewrite netlist_app_length, IHxs; simpl. apply PeanoNat.Nat.add_1_r. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib