Module ProofState_intf.S.UnitIndex

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