proposition: Lemma netlist_rev_app_distr {i j k} (xs : netlist B i j) (ys : netlist B j k) : netlist_rev flip (xs ++++ ys) = netlist_rev flip ys ++++ netlist_rev flip xs.
proof: Proof. generalize dependent i. induction xs; simpl; intros; auto. rewrite <- netlist_app_comm_cons; simpl. rewrite !netlist_rev_equation_2. rewrite IHxs. now rewrite <- netlist_app_assoc. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib