fact: Definition option_map_in_R : forall (A A' : Type) (AR : Param2a0.Rel A A') (oa : option A) (oa' : option A'), option_map A A' AR oa = oa' -> optionR A A' AR oa oa' := fun A A' AR => fun oa oa' => match oa with | Some a => match oa' with | Some a' => fun e => someR A A' AR a a' (map_in_R AR a a' (some_inj1 A' (map AR a) a' e)) | None => fun e => exfalso_option_some_none (optionR A A' AR (Some a) (None)) A' (map AR a) e end | None => match oa' with | Some a' => fun e => exfalso_option_none_some (optionR A A' AR (None) (Some a')) A' a' e | None => fun e => noneR A A' AR end end.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy