proposition: Lemma fst_snd : forall a b (z : a * b), (let '(x, y) := z in (x, y)) = (fst z, snd z).
proof: Proof. intros ? ? [?]; auto. Qed.
imports: Coq.Lists.List Category.Lib Category.Theory.Coq.Functor Category.Theory.Coq.Functor.Proofs Category.Theory.Coq.Tuple Category.Theory.Functor