Add df-iplp to iset.mm
Add df-iplp to iset.mm

The definition from the HoTT book essentially matches the one
in set.mm (when adjusted for our different definition of a
Dedekind cut).

metamath/set.mm,metamath/set.mm,metamath/set.mm