proposition: Lemma netlist_rev_unit {i j k} (xs : netlist B i j) (x : B j k) : netlist_rev flip (xs ++++ tfin x) = flip _ _ x :::: netlist_rev flip xs.
proof: Proof. induction xs; auto; simpl. rewrite <- netlist_app_comm_cons; simpl. rewrite netlist_rev_equation_2. now rewrite IHxs. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib