fact: Definition map_in_R_Bool {b b' : Bool} (e : map_Bool b = b') : BoolR b b' := match e with | idpath => match b with | false => falseR | true => trueR end end.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy