proposition: Lemma unsplit : forall a b (xs : list (a * b)), map (fun x => (fst x, snd x)) xs = xs.
proof: Proof. intros. induction xs as [|x xs IHxs]; auto; simpl. rewrite IHxs. destruct x; auto. Qed.
imports: Coq.Lists.List Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.Tuple Category.Theory.Functor