(* -*- mode: coq; mode: visual-line -*- *)
(** * Miscellaneous material *)
(** If you have a lemma or group of lemmas that you can’t find a better home for, put them here. However, big “Miscellaneous” files are sub-optimal to work with, so some caveats:
- do try to find a better home for things if possible!
- if there were any specific difficulties in placing your lemmas (eg dependency issues), please document that.
- generally, be extra-careful keeping this file well-organised and documented.
- any time you see a chance to move lemmas from this file to a better home, do so without hesitation! *)