(** %
\section{\label{sec:XXX}XXX}
% *)
Module Export patch_universes_sequences.
(** %

XXX

% *)

Require Import Arith.
Require Import Compare_dec.
Require Import Equality.
Require Import Setoid.

Require Import names.
Require Import patch_universes.
Require Import invertible_patchlike.
Require Import invertible_patch_universe.

Require Export patch_universes_sequences.many.
Require Export patch_universes_sequences.one_many.
Require Export patch_universes_sequences.many_one.
Require Export patch_universes_sequences.one_many_one.
Require Export patch_universes_sequences.many_many.

End patch_universes_sequences.