+CoInductive Fresh A T :=
+{ next : forall a:A, (T a * Fresh A T)
+; split : Fresh A T * Fresh A T
+}.
+
+
+
+
+
+Definition map2 {A}{B}(f:A->B)(t:A*A) : (B*B) := ((f (fst t)), (f (snd t))).
+
+
+(* string stuff *)
+Variable eol : string.
+Extract Constant eol => "'\n':[]".
+
+Class Monad {T:Type->Type} :=
+{ returnM : forall {a}, a -> T a
+; bindM : forall {a}{b}, T a -> (a -> T b) -> T b
+}.
+Implicit Arguments Monad [ ].
+Notation "a >>>= b" := (@bindM _ _ _ _ a b) (at level 50, left associativity).