Module ProofState_intf.S.UnitIndex

module UnitIndex: Index.UNIT_IDX 
    with type E.t = (FOTerm.t * FOTerm.t * bool * C.t)
     and type E.rhs = FOTerm.t