
diff -r 2ccf3086142b -r b5cb3183409e Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Oct 05 21:48:31 2010 +0100
+++ b/Paper/Paper.thy	Wed Oct 06 08:09:40 2010 +0100
@@ -448,12 +448,12 @@
   the identity everywhere except on a finite number of atoms. There is a 
   two-place permutation operation written
   @{text "_ \<bullet> _  ::  perm \<Rightarrow> \<beta> \<Rightarrow> \<beta>"}
-  in which the generic type @{text "\<beta>"} stands for the type of the object 
+  where the generic type @{text "\<beta>"} stands for the type of the object 
   over which the permutation 
   acts. In Nominal Isabelle, the identity permutation is written as @{term "0::perm"},
   the composition of two permutations @{term p} and @{term q} as \mbox{@{term "p + q"}}, 
   and the inverse permutation of @{term p} as @{text "- p"}. The permutation
-  operation is defined by induction over the type-hierarchy \cite{HuffmanUrban10};
+  operation is defined over the type-hierarchy \cite{HuffmanUrban10};
   for example permutations acting on products, lists, sets, functions and booleans is
   given by:
   %
@@ -611,7 +611,7 @@
   @{text as} in @{text x}, because @{term "p \<bullet> x = x"}.
 
   Most properties given in this section are described in detail in \cite{HuffmanUrban10}
-  and of course all are formalised in Isabelle/HOL. In the next sections we will make 
+  and all are formalised in Isabelle/HOL. In the next sections we will make 
   extensive use of these properties in order to define $\alpha$-equivalence in 
   the presence of multiple binders.
 *}
@@ -737,13 +737,13 @@
   \noindent
   (similarly for $\approx_{\,\textit{abs\_res}}$ 
   and $\approx_{\,\textit{abs\_list}}$). We can show that these relations are equivalence 
-  relations and equivariant.
+  relations. %% and equivariant.
 
   \begin{lemma}\label{alphaeq} 
   The relations $\approx_{\,\textit{abs\_set}}$, $\approx_{\,\textit{abs\_list}}$
-  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations, and if @{term
-  "abs_set (as, x) (bs, y)"} then also @{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet>
-  bs, p \<bullet> y)"} (similarly for the other two relations).
+  and $\approx_{\,\textit{abs\_res}}$ are equivalence relations. %, and if 
+  %@{term "abs_set (as, x) (bs, y)"} then also 
+  %@{term "abs_set (p \<bullet> as, p \<bullet> x) (p \<bullet> bs, p \<bullet> y)"} (similarly for the other two relations).
   \end{lemma}
 
   \begin{proof}
@@ -929,15 +929,15 @@
   annotated on the types are optional. Their purpose is to be used in the
   (possibly empty) list of \emph{binding clauses}, which indicate the binders
   and their scope in a term-constructor.  They come in three \emph{modes}:
-
+  %
   \begin{center}
-  \begin{tabular}{l}
-  \isacommand{bind}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
-  \isacommand{bind (set)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
-  \isacommand{bind (res)}\; {\it binders}\; \isacommand{in}\; {\it bodies}\\
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{bind} {\it binders} \isacommand{in} {\it bodies}\;\;\;\;
+  \isacommand{bind (set)} {\it binders} \isacommand{in} {\it bodies}\;\;\;\;
+  \isacommand{bind (res)} {\it binders} \isacommand{in} {\it bodies}
   \end{tabular}
   \end{center}
-
+  %
   \noindent
   The first mode is for binding lists of atoms (the order of binders matters);
   the second is for sets of binders (the order does not matter, but the
@@ -1027,17 +1027,17 @@
   \begin{equation}\label{letpat}
   \mbox{\small%
   \begin{tabular}{l}
-  \isacommand{nominal\_datatype} @{text trm} =\\
+  \isacommand{nominal\_datatype} @{text trm} $=$\\
   \hspace{5mm}\phantom{$\mid$}~@{term "Var name"}\\
   \hspace{5mm}$\mid$~@{term "App trm trm"}\\
   \hspace{5mm}$\mid$~@{text "Lam x::name t::trm"} 
      \;\;\isacommand{bind} @{text x} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let p::pat trm t::trm"} 
      \;\;\isacommand{bind} @{text "bn(p)"} \isacommand{in} @{text t}\\
-  \isacommand{and} @{text pat} =\\
-  \hspace{5mm}\phantom{$\mid$}~@{text PNil}\\
-  \hspace{5mm}$\mid$~@{text "PVar name"}\\
-  \hspace{5mm}$\mid$~@{text "PTup pat pat"}\\ 
+  \isacommand{and} @{text pat} $=$
+  @{text PNil}
+  $\mid$~@{text "PVar name"}
+  $\mid$~@{text "PTup pat pat"}\\ 
   \isacommand{binder}~@{text "bn::pat \<Rightarrow> atom list"}\\
   \isacommand{where}~@{text "bn(PNil) = []"}\\
   \hspace{5mm}$\mid$~@{text "bn(PVar x) = [atom x]"}\\
@@ -1070,14 +1070,14 @@
   \begin{equation}\label{letrecs}
   \mbox{\small%
   \begin{tabular}{@ {}l@ {}}
-  \isacommand{nominal\_datatype}~@{text "trm ="}\ldots\\
+  \isacommand{nominal\_datatype}~@{text "trm ="}~\ldots\\
   \hspace{5mm}$\mid$~@{text "Let as::assn t::trm"} 
      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text t}\\
   \hspace{5mm}$\mid$~@{text "Let_rec as::assn t::trm"}
      \;\;\isacommand{bind} @{text "bn(as)"} \isacommand{in} @{text "as t"}\\
-  \isacommand{and} @{text "ass"} =\\
-  \hspace{5mm}\phantom{$\mid$}~@{text "ANil"}\\
-  \hspace{5mm}$\mid$~@{text "ACons name trm assn"}\\
+  \isacommand{and} @{text "assn"} $=$
+  @{text "ANil"}
+  $\mid$~@{text "ACons name trm assn"}\\
   \isacommand{binder} @{text "bn::assn \<Rightarrow> atom list"}\\
   \isacommand{where}~@{text "bn(ANil) = []"}\\
   \hspace{5mm}$\mid$~@{text "bn(ACons a t as) = [atom a] @ bn(as)"}\\
@@ -1197,21 +1197,21 @@
   free-atom functions from the specification. For the 
   \emph{raw} types @{text "ty"}$_{1..n}$ we define the free-atom functions
   %
-  \begin{equation}\label{fvars}
-  @{text "fa_ty\<^isub>1, \<dots>, fa_ty\<^isub>n"}
-  \end{equation}
-
-  \noindent
+  %\begin{equation}\label{fvars}
+  @{text "fa_ty\<^isub>"}$_{1..n}$
+  %\end{equation}
+  %
+  %\noindent
   by recursion.
   We define these functions together with auxiliary free-atom functions for
   the binding functions. Given raw binding functions @{text "bn"}$_{1..m}$ 
   we define
   %
-  \begin{center}
-  @{text "fa_bn\<^isub>1, \<dots>, fa_bn\<^isub>m"}
-  \end{center}
-
-  \noindent
+  %\begin{center}
+  @{text "fa_bn\<^isub>"}$_{1..m}$.
+  %\end{center}
+  %
+  %\noindent
   The reason for this setup is that in a deep binder not all atoms have to be
   bound, as we saw in the example with ``plain'' @{text Let}s. We need therefore a function
   that calculates those free atoms in a deep binder.
@@ -1254,8 +1254,9 @@
   \noindent
   where in case @{text "d\<^isub>i"} refers to one of the raw types @{text "ty"}$_{1..n}$ from the 
   specification, the function @{text "fa_ty\<^isub>i"} is the corresponding free-atom function 
-  we are defining by recursion 
-  (see \eqref{fvars}); otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
+  we are defining by recursion; 
+  %(see \eqref{fvars}); 
+  otherwise we set @{text "fa_ty\<^isub>i d\<^isub>i = supp d\<^isub>i"}.
   
   In order to formally define the set @{text B} we use the following auxiliary @{text "bn"}-functions
   for atom types to which shallow binders may refer
@@ -1276,8 +1277,8 @@
 
   \noindent 
   Like the function @{text atom}, the function @{text "atoms"} coerces 
-  a set of atoms to a set of the generic atom type. It is defined as 
-  @{text "atoms as \<equiv> {atom a | a \<in> as}"}. 
+  a set of atoms to a set of the generic atom type. 
+  %It is defined as  @{text "atoms as \<equiv> {atom a | a \<in> as}"}. 
   The set @{text B} is then formally defined as
   %
   \begin{center}
@@ -1341,7 +1342,7 @@
   "fa\<^bsub>trm\<^esub>"}, @{text "fa\<^bsub>assn\<^esub>"} and @{text
   "fa\<^bsub>bn\<^esub>"} as follows:
   %
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
   @{text "fa\<^bsub>trm\<^esub> (Let as t)"} & @{text "="} & @{text "(fa\<^bsub>trm\<^esub> t - set (bn as)) \<union> fa\<^bsub>bn\<^esub> as"}\\
   @{text "fa\<^bsub>trm\<^esub> (Let_rec as t)"} & @{text "="} & @{text "(fa\<^bsub>assn\<^esub> as \<union> fa\<^bsub>trm\<^esub> t) - set (bn as)"}\\[1mm]
@@ -1388,7 +1389,7 @@
   "ty"}$_{1..n}$ from the specification. We write them as
   %
   %\begin{center}
-  @{text "\<approx>ty\<^isub>1, \<dots>, \<approx>ty\<^isub>n"}. 
+  @{text "\<approx>ty"}$_{1..n}$.
   %\end{center}
   %
   %\noindent
@@ -1396,7 +1397,7 @@
   define auxiliary $\alpha$-equivalence relations 
   %
   %\begin{center}
-  @{text "\<approx>bn\<^isub>1, \<dots>, \<approx>bn\<^isub>m"}
+  @{text "\<approx>bn\<^isub>"}$_{1..m}$
   %\end{center}
   %
   %\noindent
@@ -1406,9 +1407,9 @@
   %
   \begin{center}
   \begin{tabular}{r@ {\hspace{2mm}}c@ {\hspace{2mm}}l}
-  @{text "(x\<^isub>1,.., x\<^isub>n) (R\<^isub>1,.., R\<^isub>n) (x\<PRIME>\<^isub>1,.., x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
-  @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> .. \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
-  @{text "(fa\<^isub>1,.., fa\<^isub>n) (x\<^isub>1,.., x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> .. \<union> fa\<^isub>n x\<^isub>n"}\\
+  @{text "(x\<^isub>1,\<dots>, x\<^isub>n) (R\<^isub>1,\<dots>, R\<^isub>n) (x\<PRIME>\<^isub>1,\<dots>, x\<PRIME>\<^isub>n)"} & @{text "\<equiv>"} &
+  @{text "x\<^isub>1 R\<^isub>1 x\<PRIME>\<^isub>1 \<and> \<dots> \<and> x\<^isub>n R\<^isub>n x\<PRIME>\<^isub>n"}\\
+  @{text "(fa\<^isub>1,\<dots>, fa\<^isub>n) (x\<^isub>1,\<dots>, x\<^isub>n)"} & @{text "\<equiv>"} & @{text "fa\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fa\<^isub>n x\<^isub>n"}\\
   \end{tabular}
   \end{center}
 
@@ -1563,7 +1564,7 @@
   we have three relations $\approx_{\textit{trm}}$, $\approx_{\textit{assn}}$ and
   $\approx_{\textit{bn}}$ with the following clauses:
 
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "Let as t \<approx>\<^bsub>trm\<^esub> Let as' t'"}}
   {@{term "\<exists>p. (bn as, t) \<approx>lst alpha_trm fa_trm p (bn as', t')"} & @{text "as \<approx>\<^bsub>bn\<^esub> as'"}}\smallskip\\
@@ -1572,7 +1573,7 @@
   \end{tabular}
   \end{center}
 
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>assn\<^esub> ANil"}}{}\hspace{9mm}
   \infer{@{text "ACons a t as \<approx>\<^bsub>assn\<^esub> ACons a' t' as"}}
@@ -1580,7 +1581,7 @@
   \end{tabular}
   \end{center}
 
-  \begin{center}
+  \begin{center}\small
   \begin{tabular}{@ {}c @ {}}
   \infer{@{text "ANil \<approx>\<^bsub>bn\<^esub> ANil"}}{}\hspace{9mm}
   \infer{@{text "ACons a t as \<approx>\<^bsub>bn\<^esub> ACons a' t' as"}}
@@ -1615,7 +1616,7 @@
   \begin{lemma}\label{equiv} 
   Given the raw types @{text "ty"}$_{1..n}$ and binding functions
   @{text "bn"}$_{1..m}$, the relations @{text "\<approx>ty"}$_{1..n}$ and 
-  @{text "\<approx>bn"}$_{1..m}$ are equivalence relations and equivariant.
+  @{text "\<approx>bn"}$_{1..m}$ are equivalence relations.%% and equivariant.
   \end{lemma}
 
   \begin{proof} 
@@ -1721,8 +1722,10 @@
   operations defined in \eqref{ceqvt}. In order to make this 
   lifting to go through, we have to show that the permutation operations are respectful. 
   This amounts to showing that the 
-  $\alpha$-equivalence relations are equivariant, which we already established 
-  in Lemma~\ref{equiv}. As a result we can add the equations
+  $\alpha$-equivalence relations are equivariant \cite{HuffmanUrban10}.
+  %, which we already established 
+  %in Lemma~\ref{equiv}. 
+  As a result we can add the equations
   %
   \begin{equation}\label{calphaeqvt}
   @{text "p \<bullet> (C\<^sup>\<alpha> x\<^isub>1 \<dots> x\<^isub>r) = C\<^sup>\<alpha> (p \<bullet> x\<^isub>1) \<dots> (p \<bullet> x\<^isub>r)"}
@@ -1736,9 +1739,10 @@
   The latter are defined automatically for the raw types @{text "ty"}$_{1..n}$
   by the datatype package of Isabelle/HOL.
 
-  Finally we can add to our infrastructure a structural induction principle 
-  for the types @{text "ty\<AL>"}$_{i..n}$ whose 
-  conclusion of the form
+  Finally we can add to our infrastructure a cases lemma (explained in the next section)
+  and a structural induction principle 
+  for the types @{text "ty\<AL>"}$_{i..n}$. The conclusion of the induction principle is
+  of the form
   %
   \begin{equation}\label{weakinduct}
   \mbox{@{text "P\<^isub>1 x\<^isub>1 \<and> \<dots> \<and> P\<^isub>n x\<^isub>n "}}
@@ -1805,8 +1809,10 @@
   for the types @{text "ty\<AL>"}$_{1..n}$ 
   by first lifting definitions from the raw level to the quotient level and
   then by establishing facts about these lifted definitions. All necessary proofs
-  are generated automatically by custom ML-code. This code can deal with 
-  specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
+  are generated automatically by custom ML-code. 
+
+  %This code can deal with 
+  %specifications such as the one shown in Figure~\ref{nominalcorehas} for Core-Haskell.  
 
   %\begin{figure}[t!]
   %\begin{boxedminipage}{\linewidth}
@@ -2084,17 +2090,17 @@
   representations have to resort to the iterated-single-binders-approach with
   all the unwanted consequences when reasoning about the resulting terms.
 
-  Two formalisations involving general binders have been 
-  performed in older
-  versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
-  \cite{BengtsonParow09,UrbanNipkow09}).  Both
-  use the approach based on iterated single binders. Our experience with
-  the latter formalisation has been disappointing. The major pain arose from
-  the need to ``unbind'' variables. This can be done in one step with our
-  general binders described in this paper, but needs a cumbersome
-  iteration with single binders. The resulting formal reasoning turned out to
-  be rather unpleasant. The hope is that the extension presented in this paper
-  is a substantial improvement.
+  %Two formalisations involving general binders have been 
+  %performed in older
+  %versions of Nominal Isabelle (one about Psi-calculi and one about algorithm W 
+  %\cite{BengtsonParow09,UrbanNipkow09}).  Both
+  %use the approach based on iterated single binders. Our experience with
+  %the latter formalisation has been disappointing. The major pain arose from
+  %the need to ``unbind'' variables. This can be done in one step with our
+  %general binders described in this paper, but needs a cumbersome
+  %iteration with single binders. The resulting formal reasoning turned out to
+  %be rather unpleasant. The hope is that the extension presented in this paper
+  %is a substantial improvement.
  
   The most closely related work to the one presented here is the Ott-tool
   \cite{ott-jfp} and the C$\alpha$ml language \cite{Pottier06}. Ott is a nifty
@@ -2119,36 +2125,38 @@
   binding clauses. In Ott you specify binding clauses with a single body; we 
   allow more than one. We have to do this, because this makes a difference 
   for our notion of $\alpha$-equivalence in case of \isacommand{bind (set)} and 
-  \isacommand{bind (res)}. Consider the examples
+  \isacommand{bind (res)}. 
 
-  \begin{center}
-  \begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
-  @{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
-  @{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
-      \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
-  \end{tabular}
-  \end{center}
+  %Consider the examples
+  %
+  %\begin{center}
+  %\begin{tabular}{@ {}l@ {\hspace{2mm}}l@ {}}
+  %@{text "Foo\<^isub>1 xs::name fset t::trm s::trm"} &  
+  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t s"}\\
+  %@{text "Foo\<^isub>2 xs::name fset t::trm s::trm"} &  
+  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "t"}, 
+  %    \isacommand{bind (set)} @{text "xs"} \isacommand{in} @{text "s"}\\
+  %\end{tabular}
+  %\end{center}
+  %
+  %\noindent
+  %In the first term-constructor we have a single
+  %body that happens to be ``spread'' over two arguments; in the second term-constructor we have
+  %two independent bodies in which the same variables are bound. As a result we 
+  %have
+  % 
+  %\begin{center}
+  %\begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
+  %@{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & 
+  %@{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
+  %@{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
+  %@{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
+  %\end{tabular}
+  %\end{center}
 
   \noindent
-  In the first term-constructor we have a single
-  body that happens to be ``spread'' over two arguments; in the second term-constructor we have
-  two independent bodies in which the same variables are bound. As a result we 
-  have
-
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{1.5mm}}c@ {\hspace{1.5mm}}l}
-  @{text "Foo\<^isub>1 {a, b} (a, b) (a, b)"} & $\not=$ & 
-  @{text "Foo\<^isub>1 {a, b} (a, b) (b, a)"}\\
-  @{text "Foo\<^isub>2 {a, b} (a, b) (a, b)"} & $=$ & 
-  @{text "Foo\<^isub>2 {a, b} (a, b) (b, a)"}\\
-  \end{tabular}
-  \end{center}
-
-  \noindent
-  and therefore need the extra generality to be able to distinguish between 
-  both specifications.
+  %and therefore need the extra generality to be able to distinguish between 
+  %both specifications.
   Because of how we set up our definitions, we also had to impose some restrictions
   (like a single binding function for a deep binder) that are not present in Ott. Our
   expectation is that we can still cover many interesting term-calculi from
@@ -2187,10 +2195,11 @@
   $\alpha$-equivalence and automated all necessary proofs in Isabelle/HOL.
   To specify general binders we used the specifications from Ott, but extended them 
   in some places and restricted
-  them in others so that they make sense in the context of $\alpha$-equated terms. We also introduced two binding modes (set and res) that do not 
+  them in others so that they make sense in the context of $\alpha$-equated terms. 
+  We also introduced two binding modes (set and res) that do not 
   exist in Ott. 
   We have tried out the extension with terms from Core-Haskell, type-schemes 
-  and the lambda-calculus, and our code
+  and a dozen of other calculi from programming language research. The code
   will eventually become part of the next Isabelle distribution.\footnote{For the moment
   it can be downloaded from the Mercurial repository linked at
   \href{http://isabelle.in.tum.de/nominal/download}
@@ -2204,31 +2213,31 @@
   definitions to equivariant functions (for such functions it is possible to
   provide more automation).
 
-  There are some restrictions we imposed in this paper that we would like to lift in
-  future work. One is the exclusion of nested datatype definitions. Nested
-  datatype definitions allow one to specify, for instance, the function kinds
-  in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
-  version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
-  achieve this, we need a slightly more clever implementation than we have at the moment. 
+  %There are some restrictions we imposed in this paper that we would like to lift in
+  %future work. One is the exclusion of nested datatype definitions. Nested
+  %datatype definitions allow one to specify, for instance, the function kinds
+  %in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
+  %version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
+  %achieve this, we need a slightly more clever implementation than we have at the moment. 
 
-  A more interesting line of investigation is whether we can go beyond the 
-  simple-minded form of binding functions that we adopted from Ott. At the moment, binding
-  functions can only return the empty set, a singleton atom set or unions
-  of atom sets (similarly for lists). It remains to be seen whether 
-  properties like
+  %A more interesting line of investigation is whether we can go beyond the 
+  %simple-minded form of binding functions that we adopted from Ott. At the moment, binding
+  %functions can only return the empty set, a singleton atom set or unions
+  %of atom sets (similarly for lists). It remains to be seen whether 
+  %properties like
+  %%
+  %\begin{center}
+  %@{text "fa_ty x  =  bn x \<union> fa_bn x"}.
+  %\end{center}
   %
-  \begin{center}
-  @{text "fa_ty x  =  bn x \<union> fa_bn x"}.
-  \end{center}
-  
-  \noindent
-  allow us to support more interesting binding functions. 
-
-  We have also not yet played with other binding modes. For example we can
-  imagine that there is need for a binding mode 
-  where instead of lists, we abstract lists of distinct elements.
-  Once we feel confident about such binding modes, our implementation 
-  can be easily extended to accommodate them.
+  %\noindent
+  %allow us to support more interesting binding functions. 
+  %
+  %We have also not yet played with other binding modes. For example we can
+  %imagine that there is need for a binding mode 
+  %where instead of lists, we abstract lists of distinct elements.
+  %Once we feel confident about such binding modes, our implementation 
+  %can be easily extended to accommodate them.
 
   \medskip
   \noindent




