proposition: Lemma compose_snd_prod : snd o (a * b) = b.
proof: Proof. path_functor; trivial. Defined.
imports: Category.Core Functor.Core Category.Prod Functor.Composition.Core Functor.Prod.Core Functor.Paths Types.Prod HoTT.Tactics Types.Forall Types.Sigma Basics.Tactics