show a Proper instance for dom

I think we also want a version:

Proper ((≡@{M A}) ==> (=)) (dom D).

when LeibnizEquiv D.

Good point, though I haven't seen similar instances before. Not sure where else they would apply though.

That should then probably be preferred over the other version?

though I haven't seen similar instances before.

We have things like length_proper

added 1 commit

• 6aaefb52 - stronger proper for domains with leibniz equality

Compare with previous version

That should then probably be preferred over the other version?

Yes, I think so if you want f_equiv to work well. (That makes no sense)

We have things like length_proper

Well that's different, that does not have two overlapping instances.

Yes, I think so if you want f_equiv to work well.

f_equiv starts with a known relation for the result, so I don't think it is affected by this priority.

The idea was that in a situation like a \in dom _ map, if possible it should use the leibniz-version of proper so that it doesn't even need a proper for \in.

I added dom_proper_L.

added 1 commit

• 330c3e94 - fix comment nits

Compare with previous version

resolved all discussions

mentioned in commit 77eecb3c

merged

Merged, thanks.