RecoverExample.v: toy proof that might help with [atomic_cp_recover_ok]
RecoverExample.v: toy proof that might help with [atomic_cp_recover_ok]

why this is interesting:

- the [work] function has a crash condition consisting of 3 OR cases
- the [recover] function has a precondition / crash condition consisting
  of just one case (i.e., matching only one of the OR cases)
- the [corr3] theorem has a recovery condition that has 2 (not 3) OR cases
  corresponding to the 3 OR cases from [work]'s crash condition; there are
  2 instead of 3 because [recover] collapses two of the original ORs into
  a single post-recovery state.
- the proof does no explicit instantiation of evars.

one conclusion is that it should OK to have AtomicCp's [recover] with a
simple spec that has only a single diskset in the precondition, and we
should be able to instantiate things so that we get several OR cases in
the resulting [corr3] theorem [atomic_cp_with_recover_ok].

mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl,mit-pdos/fscq-impl