diff --git a/content/separated-nominal-automata.tex b/content/separated-nominal-automata.tex
index 9864c70..7cb396d 100644
--- a/content/separated-nominal-automata.tex
+++ b/content/separated-nominal-automata.tex
@@ -159,11 +159,23 @@ Moreover, recall that every $\sb$-set is also a $\perm$-set; the associated noti
 In particular, this means that the forgetful functor restricts to $U \colon \sbnom \to \permnom$.
 
 \startlemma[reference=lem:GM-support]
-(Theorem 4.8 from \citet[Gabbay07])
+(Theorem 4.8 from \citenp[Gabbay07])
 Let $X$ be a nominal $\sb$-set, $x \in X$, and $C \subset \atoms$.
 Then $C$ is an $\sb$-support of $x$ iff it is a $\perm$-support of $x$.
 \stoplemma
 
+\startremark
+It is not true that any $\perm$-support is an $\sb$-support.
+The condition that $X$ is nominal, in the above lemma, is crucial.
+Let $X = \atoms + 1$ and define the following $\sb$-action: $m \cdot a = m(a)$ if $m$ is injective, $m \cdot a = \ast$ if $m$ is non-injective, and $m \cdot \ast = \ast$.
+This is a well-defined $\sb$-set, but is \emph{not nominal}.
+Now consider $U(X)$, this is the $\perm$-set $\atoms + 1$ with the natural action, which is a \emph{nominal} $\perm$-set!
+In particular, as a $\perm$-set each element has a finite support, but as a $\sb$-set the supports are infinite.
+
+This counterexample is similar to the exploding nominal sets of \citet[Gabbay07], but even worse behaved.
+We like to call them \emph{nuclear sets}, since an element will collapse when hit by a non-injective map, no matter how far away the non-injectivity occurs.
+\stopremark
+
 For $M \in \{\sb, \perm\}$, any element $x \in X$ of a nominal $M$-set $X$ has a least finite support (w.r.t. set inclusion).
 We denote the least finite support of an element $x \in X$ by $\supp(x)$.
 Note that by \in{Lemma}[lem:GM-support], the set $\supp(x)$ is independent of whether a nominal $\sb$-set $X$ is viewed as an $\sb$-set or a $\perm$-set.
@@ -256,7 +268,6 @@ $U$ maps the exponent object in $\sbnom$ to the right adjoint $\wandto$ of the s
 \stopitemize
 
 Together, these results form the categorical infrastructure to relate nominal languages to separated languages and automata in \in{Section}[sec:automata].
-\todo{Reconsider moving some proofs from the appendix to the main text}.
 
 \startdefinition[reference=def:left-adjoint]
 Given a $\perm$-nominal set $X$, we define a nominal $\sb$-set $F(X)$ as follows.
@@ -293,6 +304,45 @@ The construction $F$ in \in{Definition}[def:left-adjoint] extends to a functor
 defined on an equivariant map $f \colon X \to Y$ by $F(f)([m, x]) = [m, f(x)] \in F(Y)$.
 \stopproposition
 
+\startproofnoqed
+\startdescription{$F(X)$ is an $\sb$-set.}
+We first check whether the $\sb$-action is well-defined.
+Let $[m_1, x_1] = [m_2, x_2] \in F(X)$ and let $m \in \sb$.
+By \in{Lemma}[lm:sim], there is some permutation $g$ such that  $g x_1 = x_2$
+and $m_1|_C = m_2 g|_C$ for some support $C$ of $x_1$.
+By post-composition with $m$ we get $m m_1|_C = m m_2 g|_C$, which means (again by the lemma)
+that $[m m_1, x_1] = [m m_2, x_2]$.
+Thus $m [m_1, x_1] = m [m_2, x_2]$, which concludes well-definedness.
+
+For associativity and unitality of the $\sb$-action, we simply note that it is
+directly defined by left multiplication of $\sb$ which is associative and unital.
+This concludes that $F(X)$ is an $\sb$-set.
+\stopdescription
+\startdescription{$F(X)$ is an $\sb$-nominal set.}
+Given an element $[m, x] \in F(X)$ and a $\perm$-support $C$ of $x$, we will prove that $m \cdot C$ 
+is an $\sb$-support for $[m, x]$.
+Suppose that we have $m_1, m_2 \in \sb$ such that $m_1|_{m\cdot C} = m_2|_{m\cdot C}$.
+By pre-composition with $m$ we get $m_1 m|_C = m_2 m|_C$ and this leads us to conclude $[m_1 m, x] = [m_2 m, x]$.
+So $m_1 [m,x] = m_2 [m, x]$ as required.
+\stopdescription
+\startdescription{Functoriality.}
+Let $f \colon X \to Y$ be a $\perm$-equivariant map.
+To see that $F(f)$ is well-defined consider $[m_1, x_1] = [m_2, x_2]$.
+By \in{Lemma}[lm:sim], there is a permutation $g$ such that  $g x_1 = x_2$
+and $m_1|_C = m_2 g|_C$ for some support $C$ of $x_1$.
+Applying $F(f)$ gives on one hand $[m_1, f(x_1)]$ and
+on the other hand $[m_2, f(x_2)] = [m_2, f(g x_1)] = [m_2, g f(x_1)] = [m_2 g, f(x_1)]$
+(we used equivariance in the second step). Since $m_1|_C = m_2 g|_C$ and $f$ preserves supports
+we have $[m_2 g, f(x_1)] = [m_1, f(x_1)]$.
+
+For $\sb$-equivariance we consider both $n \cdot F(f)([m, x]) = n [m, f(x)] = [n m, f(x)]$ and $F(f)(n \cdot [m, x]) = F(f)([nm, x]) = [nm, f(x)]$.
+This shows that $n F(f)([m, x]) = F(f)(n [m, x])$ and concludes that we have a map $F(f) \colon F(X) \to F(Y)$.
+
+The fact that $F$ preserves the identity function and composition follows from the definition directly.
+\QED
+\stopdescription
+\stopproofnoqed
+
 \starttheorem[reference=thm:adjunction]
 The functor $F$ is left adjoint to $U$:
 \placefigure[force, none]{}{
@@ -334,19 +384,19 @@ The functor $F$ not only preserves coproducts, being a left adjoint, but
 it also maps the separated product to products:
 
 \starttheorem[reference=thm:monoidal]
-The functor $F$ is strong monoidal, from the monoidal category $(\permset, \sepprod, 1)$ to $(\sbset, \times, 1)$.
+The functor $F$ is strong monoidal, from the monoidal category\break $(\permset, \sepprod, 1)$ to $(\sbset, \times, 1)$.
 In particular, the map $p$ given by
 \startformula
 p = \langle F(\pi_1), F(\pi_2) \rangle \colon F(X \sepprod Y) \to F(X) \times F(Y)
 \stopformula
 is an isomorphism, natural in $X$ and $Y$.
 \stoptheorem
-\startproof
+\startproofnoqed
 We prove that $p$ is an isomorphism.
 It suffices to show that $p$ is injective and surjective.
 Note that $p([m, (x, y)]) = ([m, x], [m, y])$.
 
-\startdescription[title={Surjectivity}]
+\startdescription[title={Surjectivity.}]
 Let $([m_1, x], [m_2, y])$ be an element of $F(X) \times F(Y)$.
 We take an element $y' \in Y$ such that $y' \separated \supp(x)$ and $y' = gy$ for some $g \in \perm$.
 Now we have an element $(x, y') \in X \sepprod Y$.
@@ -372,7 +422,7 @@ and since $[mg, y] = [m, g y] = [m, y']$ we are done.
 Hence $p([m, (x, y')]) = ([m, x], [m, y']) = ([m_1, x], [m_2, y])$, so $p$ is surjective.
 \stopdescription
 
-\startdescription[title={Injectivity}]
+\startdescription[title={Injectivity.}]
 Let $[m_1, (x_1, y_1)]$ and $[m_2, (x_2, y_2)]$ be two elements.
 Suppose that they are mapped to the same element, i.e., $[m_1, x_1] = [m_2, x_2]$ and $[m_1, y_1] = [m_2, y_2]$.
 Then there are permutations $g_x, g_y$ such that $x_2 = g_x x_1$ and $y_2 = g_y y_1$.
@@ -394,12 +444,13 @@ We also obtain $m_1|_{C \cup D} = m_2 g|_{C \cup D}$.
 This proves that $[m_1, (x_1, y_1)] = [m_2, (x_2, y_2)]$, and so the map $p$ is injective.
 \stopdescription
 
-\startdescription[title={Unit and coherence}]
+\startdescription[title={Unit and coherence.}]
 To show that $F$ preserves the unit, we note that $[m, 1] = [m', 1]$ for every $m, m' \in \sb$, as the empty set supports $1$ and so $m|_{\emptyset} = m'|_{\emptyset}$ vacuously holds.
 We conclude $F(1)$ is a singleton.
 By the definition $p([m, (x, y)])=([m, x], [m, y])$, one can check the coherence axioms elementary.
+\QED
 \stopdescription
-\stopproof
+\stopproofnoqed
 
 Since $F$ also preserves coproducts (being a left adjoint), we obtain that $F$ maps the set of separated words to the set of all words.
 \startcorollary[reference=cor:sep-words]
@@ -418,7 +469,18 @@ Concretely, for $X \in \permnom$ and $Y \in \sbnom$:
 \stopitemize
 \stoplemma
 
-To appreciate the above result, we give a concrete characterisation of one-dimensional nominal sets:
+The first item follows easily by showing that $\eta$ is surjective.
+However, the second is non-trivial and uses the following technical property of $\leq 1$-dimensional $\sb$-sets.
+
+\startlemma[reference=lem:1dim-sbnom]
+Let $Y$ be a nominal $\sb$-set.
+If an element $y \in Y$ is supported by a singleton set (or even the empty set), then
+\startformula
+\{ m y \mid m \in \sb \} = \{ g y \mid g \in \perm \} .
+\stopformula
+\stoplemma
+
+To appreciate the above results, we give a concrete characterisation of one-dimensional nominal sets:
 \startlemma[reference=lm:char-dim-one]
 Let $X$ be a nominal $M$-set, for $M \in \{\sb,\perm\}$.
 Then $\dim(X) \leq 1$ iff there exist (discrete) sets $Y$ and $I$ such that $X \cong Y + \coprod_{I} \atoms$.
@@ -445,11 +507,27 @@ We define a $\perm$-equivariant map $\phi$ as follows:
 \startformula
 \phi \colon (X \wandto U(Y)) \to U(F(X) \sbto Y)
 \stopformula
-is defined by transposing (first by Currying, then by the adjunction) the following composition
+is defined by using the composition
 \startformula
-F(X \wandto U(Y)) \times F(X) \xrightarrow{p^{-1}} F((X \wandto U(Y)) \sepprod X) \xrightarrow{F(\ev)} FU(Y) \xrightarrow{\epsilon} Y
+F(X \wandto U(Y)) \times F(X) \tot{p^{-1}} F((X \wandto U(Y)) \sepprod X) \tot{F(\ev)} FU(Y) \tot{\epsilon} Y,
 \stopformula
 where $p^{-1}$ is from \in{Theorem}[thm:monoidal] and $\ev$ is the evaluation map of the exponent $\wandto$.
+By Currying and the adjunction we arrive at $\phi$:
+
+\placefigure[force,none]{}{
+\hbox{\starttikzpicture[node distance=16pt]
+\node              (1) {$F(X \wandto U(Y)) \times F(X) \to Y$};
+\node [below of=1] (2) {$F(X \wandto U(Y)) \to (F(X) \sbto Y)$};
+\node [below of=2] (3) {$(X \wandto U(Y)) \to U(F(X) \sbto Y)$};
+\node [fit=(1) (2), inner sep=1pt] (12) {};
+\node [fit=(2) (3), inner sep=1pt] (23) {};
+
+\node [anchor=west] at (12.east) {by Currying};
+\node [anchor=west] at (23.east) {by \in{Theorem}[thm:adjunction]};
+
+\draw (12.west) -- (12.east);
+\draw (23.west) -- (23.east);
+\stoptikzpicture}}
 \stopdefinition
 
 With this map we can prove a generalisation of \in{Theorem}[thm:adjunction].
@@ -460,6 +538,39 @@ Second, it extends the correspondence to all finitely supported maps and not jus
 \starttheorem[reference=thm:exponent-separated]
 The sets $X \wandto U(Y)$ and $U(F(X) \sbto Y)$ are naturally isomorphic via $\phi$ as nominal $\perm$-sets.
 \stoptheorem
+\startproof
+We define some additional maps in order to construct the inverse of $\phi$.
+First, from \in{Theorem}[thm:adjunction] we get the following isomorphism:
+\startformula
+q \colon U(X \times Y) \tot{=} U(X) \times U(Y)
+\stopformula
+Second, with this map and Currying, we obtain the following two natural maps:
+
+\placefigure[force,none]{}{
+\hbox{\starttikzpicture[node distance=16pt]
+\node              (1) {$U(F(X) \sbto Y) \times UF(X) \tot{q^{-1}} U((F(X) \sbto Y) \times F(X)) \tot{U(\ev)} U(Y)$};
+\node [below of=1] (2) {$\alpha \colon U(F(X) \sbto Y) \to (UF(X) \permto U(Y))$};
+\node [fit=(1) (2), inner sep=1pt] (12) {};
+
+\node [anchor=west] at (12.east) {by Currying};
+
+\draw (12.west) -- (12.east);
+\stoptikzpicture}}
+
+\placefigure[force,none]{}{
+\hbox{\starttikzpicture[node distance=16pt]
+\node              (1) {$(UF(X) \permto U(Y)) \times X \tot{\id {\times} \eta} (UF(X) \permto U(Y)) \times UF(X) \tot{\ev} U(Y)$};
+\node [below of=1] (2) {$\beta \colon (UF(X) \permto U(Y)) \to (X \permto U(Y))$};
+\node [fit=(1) (2), inner sep=1pt] (12) {};
+
+\node [anchor=west] at (12.east) {by Currying};
+
+\draw (12.west) -- (12.east);
+\stoptikzpicture}}
+
+A calculation shows that $r \circ \beta \circ \alpha$ is the inverse of $\phi$.
+\footnote{We use $r_{X, U(Y)} \colon (X \permto U(Y)) \to (X \wandto U(Y))$ here.}
+\stopproof
 
 Note that this theorem gives an alternative characterisation of the magic wand in terms of the exponent in $\sbnom$, if the codomain is $U(Y)$.
 Moreover, for a $1$-dimensional object $X$ in $\sbnom$, we obtain the following special case of the theorem (using the co-unit isomorphism from \in{Lemma}[lem:1dim-iso]):
@@ -642,7 +753,24 @@ Then $\overline{S}(a_1a_2a_3\cdots a_n) = m \cdot S(b_1 b_2 b_3 \cdots b_n)$.
 \stoptheorem
 \startproof
 There is the following chain of one-to-one correspondences, from the results of the previous section:
-\todo{Chain of one-to-one correspondences}.
+\placefigure[force,none]{}{
+\hbox{\starttikzpicture[node distance=16pt]
+\node              (1) {$(U\Sigma)^{(*)} \rightarrow UO$};
+\node [below of=1] (2) {$F(U\Sigma)^{(*)} \rightarrow O$};
+\node [below of=2] (3) {$(FU\Sigma)^* \rightarrow O$};
+\node [below of=3] (4) {$\Sigma^* \rightarrow O$};
+\node [fit=(1) (2), inner sep=1pt] (12) {};
+\node [fit=(2) (3), inner sep=1pt] (23) {};
+\node [fit=(3) (4), inner sep=1pt] (34) {};
+
+\node [anchor=west] at (12.east) {by {\in{Theorem}[thm:adjunction]} };
+\node [anchor=west] at (23.east) {by {\in{Corollary}[cor:sep-words]} };
+\node [anchor=west] at (34.east) {by {\in{Lemma}[lem:1dim-iso]} };
+
+\draw (12.west) -- (12.east);
+\draw (23.west) -- (23.east);
+\draw (34.west) -- (34.east);
+\stoptikzpicture}}
 \stopproof
 
 Thus, every separated automaton over $U(\Sigma), U(O)$ gives rise to an $\sb$-language $\overline{S}$, corresponding to the language $S$ accepted by the automaton.
@@ -653,7 +781,10 @@ Hence, in such a case, the restricted separated automaton suffices to describe t
 
 \startdefinition[reference=def:restr-aut]
 Let $i \colon Q \sepprod U(\Sigma) \to Q \times U(\Sigma)$ be the natural inclusion map.
-A nominal automaton $\mathcal{A} = (Q, \delta, o, q_0)$ induces a separated automaton $\mathcal{A}_*$, by setting $\mathcal{A}_* = (Q, \delta \circ i, o, q_0)$.
+A nominal automaton $\mathcal{A} = (Q, \delta, o, q_0)$ induces a separated automaton $\mathcal{A}_*$, by setting
+\startformula
+\mathcal{A}_* = (Q, \delta \circ i, o, q_0).
+\stopformula
 \stopdefinition
 
 \starttheorem[reference=thm:separated-sb-lang]