fact: Definition prod_map (A A' : Type) (AR : Param10.Rel A A') (B B' : Type) (BR : Param10.Rel B B') : A * B -> A' * B' := fun p => match p with | (a, b) => (map AR a, map BR b) end.
imports: Coq(ssreflect) HoTT(HoTT) Hierarchy