proposition: Lemma netlist_rev_involutive {i j} (xs : netlist B i j) : netlist_rev flip (netlist_rev flip xs) = xs.
proof: Proof. Proof using A B flip flip_involutive. induction xs; simpl; auto. - rewrite !netlist_rev_equation_1. now rewrite flip_involutive. - rewrite netlist_rev_equation_2. rewrite netlist_rev_app_distr. rewrite IHxs. rewrite netlist_rev_equation_1. now rewrite flip_involutive. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib