Show that the solution of the COFE solver is inhabited.

Following the discussion here: https://mattermost.mpi-sws.org/iris/pl/y8igjzdnj7fzmbpbci4a4hb1ka

Note that we do not get this for free. Take F X := ▶ X, then a possible solution is Empty_set:

Lemma foo : ofe_iso Empty_set (later Empty_set).
Proof.
  assert (NonExpansive (@later_car Empty_set)) by (intros ? [[]]).
  refine (OfeIso (OfeMor Next) (OfeMor later_car) _ _).
  - intros [[]].
  - intros [].
Qed.

changed the description

added 2 commits

• 78a977a5 - Show that the solution of the COFE solver is inhabited.
• 66b36c53 - CHANGELOG.

Compare with previous version

Makes sense, thanks. :)

mentioned in commit a2db91f9

merged