fact: Definition R_in_mapK_Empty : forall (e e' : Empty) (eR : EmptyR e e'), map_in_R_Empty e e' (R_in_map_Empty e e' eR) = eR := fun e => match e with end.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy