fact: Definition Param_Bool_sym_inv {b b' : Bool} (bR : BoolR b b') : Param_Bool_sym (Param_Bool_sym bR) = bR := match bR with | falseR => idpath | trueR => idpath end.
imports: Coq(ssreflect) HoTT(HoTT) HoTT_additions Hierarchy