- Propagated changes to the modified Coq file
- Propagated changes to extractable file
- Fixed the following things:
  * Now the extractable relation takes the selection as a parameter
  * However, it is unable to "guess" the selection parameter to pass
downstream, therefore I introduced a coinductive datatype selectstar,
which describes the full (infinite) downstream path if needed (it is
only needed for trees of forks). This makes this change fairly complex
in theory
- Performed full extraction, but it appears the full extractable
semantics is too big for the extraction plugin (stack overflows and
broken pipes all over). Therefore I have done it piece-by-piece (see
extractedPieces.txt) which I will hand reassemble.