proposition: Lemma netlist_cons_uncons {i m j} (xs : netlist B i j) (y : B i m) ys : netlist_uncons xs = existT2 _ _ _ y (Some ys) → xs = y :::: ys.
proof: Proof. Proof using A B inj_pair2. destruct xs; simpl; intros. - inversion H. - inversion H; subst; clear H. apply inj_pair2 in H2; auto. apply inj_pair2 in H3; auto. now rewrite H2, H3. Qed.
imports: Coq.Bool.Bool Coq.Lists.List Equations(Equations) Category.Lib