(* -*- 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! *)Local Open Scope path_scope. (** Currently there is nothing here. *)