The previous commit is not really necesarry anymore, but my proof
for UIP of types with decidable equality is a bit more general, so
I won't revert it.

This way we get rid of the (unused) axiom eq_rect_eq reported by coqchk.

This requirement was useful in Iris 2.0: in order to ensure that ownership of
the physical state was timeless, we required the ghost CMRA to have a timeless
unit. To avoid having additional type class parameters, or having to extend the
algebraic hierarchy, we required the units of any CMRA to be timeless.

In Iris 3.0, this issue no longer applies: ownership of the physical state is
ghost ownership in the global CMRA, whose unit is always timeless.

Thanks to Jeehoon Kang for spotting this unnecessary requirement.

There is still the reals stuff, which is caused by importint Psatz (needed
for lia) and eq_rect_eq which is caused by importint Eqdep_dec.

Unfortunately, it still fails in iris.prelude.pretty.pretty_N_inj

Fixes #28

docs: fix bug in ghost resource laws

I think the current rule if buggy; the validity of a ghost resource `a` should not imply its ownership.

Please advise me if I understand incorrectly :-)  Thank you!
Jeehoon

See merge request !5

docs: fix bug in ghost resource laws

I think the current rule if buggy; the validity of a ghost resource `a` should not imply its ownership.

Please advise me if I understand incorrectly :-)  Thank you!
Jeehoon

See merge request !5

This is more consistent with the definition of the extension order, which
is also defined in terms of an existential.

It is not non-expansive, so not a function we should use.

They are redundant because frac is discrete.

fix typo

@jung good?

See merge request !2