--- /dev/null
+(***********************************************************************************************************************************
+ *
+ * This is the Coq development accompanying
+ *
+ * __Multi-Level Programs are Generalized Arrows__
+ *
+ * Best viewed on a 132-character-wide display (use the first line of this file to size your window)
+ *
+ * This file makes extensive use of Unicode (UTF-8); please make sure your text editor supports it.
+ *
+ * Here is the version of Coq I used:
+ *
+ * megacz@skolem:~$ coqc -v
+ * The Coq Proof Assistant, version 8.3pl1 (March 2011)
+ * compiled on Mar 17 2011 21:07:25 with OCaml 3.11.2
+ *
+ * Warning: this script may take a half-hour or more to typecheck, even on a very fast machine.
+ * It also needs about 1.5GB of ram; if you have less than that it will run unbearably slowly.
+ *
+ * I recommend checking it using the following command:
+ *
+ * coqc -noglob -dont-load-proofs GArrows.v
+ *
+ **********************************************************************************************************************************)
+
+Require Import Coq.Unicode.Utf8.
+Require Import Coq.Classes.RelationClasses.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Setoids.Setoid.
+Require Setoid.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Omega.