fact: Definition map_in_R {A B} (R : Param2a0.Rel A B) : forall (a : A) (b : B), map R a = b -> R a b := Map2a.map_in_R _ (Param2a0.covariant A B R).
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Database elpi(elpi)