\section{Further details on Dfn.~\ref{dfn:translation-of-proofs}, Sect.~\ref{sect:wfm}}
\label{sect:app-wfm}

%\paragraph*{Further details on Dfn.~\ref{dfn:translation-of-proofs}}
			The initial steps of $\arith$ are translated as follows,
			\[
			\begin{array}{ccc}
%			\vlinf{\word_\epsilon}{}{\seqar \word (\epsilon)}{}
%			& : &
%			\epsilon
%			\\ 
			\vlinf{\genzer}{}{\word(t) \seqar \word(\succ_0 t)}{}
			& \quad :\quad  &
			\succ_0 ( ;x) 
			\\
			\vlinf{\genone}{}{\word(t) \seqar \word(\succ_1 t)}{}
			& \quad : \quad & 
			\succ_1 (; x)
			\\
%			\vlinf{\epsilon^0}{}{ \word (t)  , \epsilon = \succ_0 t \seqar }{} 
%			& : &
%			\epsilon
%			\\
%			\vlinf{\epsilon^1}{}{ \word (t)  , \epsilon = \succ_1 t \seqar }{}
%			& : &
%			\epsilon
%			\\
%			\vlinf{\succ_0}{}{\word (s) , \word (t)  , \succ_0 s = \succ_0 t\seqar s = t }{}
%			& : &
%			\epsilon
%			\\
%			\vlinf{\succ_1}{}{\word (s) , \word (t)  , \succ_1 s = \succ_1 t\seqar s = t }{}
%			& : &
%			\epsilon
%			\\
%			\vlinf{\inj}{}{\word(t), \succ_0 t = \succ_1 t \seqar}{}
%			& : &
%			\epsilon
%			\\
			\vlinf{\surj}{}{\word (t) \seqar t = \epsilon \laor \exists y^\word . t = \succ_0 y \laor \exists y^\word. t = \succ_1 y }{}
			&\quad : \quad  &
			( \epsilon , \pred (  ;x) , \pred (;x ) )
			\\
				\vlinf{\wordcntr}{}{\word(t) \seqar \word(t) \land \word(t) }{}
				& \quad  : \quad &
				( \id (;x) , \id (;x) )
			\end{array}
			\]
			and the remaining initial steps are translated to $\epsilon$.
			
			
					Suppose $\pi$ ends with a $\rigrul{\land}$ step:
						\[
						\vlderivation{
							\vliin{\land}{}{ \Gamma, \Sigma \seqar \Delta, \Pi, A\land B }{
								\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
							}{
							\vltr{\pi_2}{ \Sigma \seqar \Pi, B }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
						}
					}
					\]
					By the inductive hypothesis let us suppose we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y)$ from $\pi_1$ and $\pi_2$ respectively, where $\type\left( \bigotimes\Gamma \right) = (\vec u; \vec x)$ and $\type \left( \bigotimes \Sigma \right) = (\vec v ; \vec y)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ and $\vec h = (\vec h^\Pi , \vec h^B)$, to denote the $\Delta$ and $A$ parts of $\vec g$ and the $\Pi$ and $B$ parts of $\vec h$.
					%	So we have $\vec f^{1} (\vec x ; \vec a)$ and $\vec f^2 (\vec y ; \vec b)$ for $\pi_1 $ and $\pi_2$ respectively, by the inductive hypothesis. 
			
			
			
			
			
			
					We construct $\vec f^\pi$ by simply rearranging these tuples of functions:
					\[
					\vec f^\pi (\vec u , \vec v ; \vec x , \vec y)
					\quad := \quad
					\left(
					\vec g^\Delta (\vec u ; \vec x) , \vec h^\Pi (\vec v ; \vec y)  , \vec g^A (\vec u ; \vec x) , \vec h^B (\vec v ; \vec y)
					\right)
					\] 
					
					
						If $\pi$ ends with a $\lefrul{\exists}$ step,
									\[
									\vlderivation{
										\vlin{\lefrul{\exists}}{}{ \Gamma, \exists x^\word . A(x) \seqar \Delta }{
											\vltr{\pi'}{ \Gamma , A(a),  \word(a) \seqar \Delta  }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
										}
									}
									\]
									then $\vec f^{\pi}$ is exactly the same as $\vec f^{\pi'}$.
									
										
											Suppose $\pi$ ends with a $\cut$ step:
											\[
											\vlderivation{
												\vliin{\cut}{}{\Gamma , \Sigma \seqar \Delta , \Pi}{
													\vltr{\pi_1}{ \Gamma \seqar \Delta, A }{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
												}{
												\vltr{\pi_2}{\Sigma , A \seqar \Pi}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
											}
										}
										\]
										
										We have two cases. First, if $A$ is free of modalities, then $\type (A)$ consists of only safe inputs. Therefore we have functions $\vec g (\vec u; \vec x)$ and $\vec h (\vec v ; \vec y, \vec z)$ from $\pi_1$ and $\pi_2 $ respectively, such that $\type(\Gamma) = (\vec u ; \vec x)$, $\type(\Sigma) = (\vec v ; \vec y )$ and $\type (A) = (;\vec z)$. Let us write $\vec g = (\vec g^\Delta , \vec g^A)$ as before, and we define $\vec f^\pi$ as follows:
										
										\[
										\vec f^\pi ( \vec u , \vec v ; \vec x, \vec y)
										\quad := \quad
										\left(
										\vec g^\Delta (\vec u ; \vec x) 
										,
										\vec h ( \vec v ; \vec y , \vec g^A ( \vec u ; \vec x ) )
										\right)
										\]
										Notice that all safe inputs on the left occur hereditarily safe on the right, and so these expressions are definable in BC by Prop.~\ref{prop:bc-properties}.
										
										
										
										
											Suppose $\pi$ ends with a $\lefrul{\cntr}$ step,
												\[
												\vlderivation{
													\vlin{\lefrul{\cntr}}{}{ !A , \Gamma \seqar \Delta }{
														\vltr{\pi'}{  !A, !A , \Gamma \seqar \Delta}{\vlhy{\quad }}{\vlhy{ }}{\vlhy{\quad }}
													}
												}
												\]
												so we have functions $\vec f' ( \vec u^1, \vec u^2 , \vec v ; \vec x)$, with $\vec u^1$ and $\vec u^2$ corresponding to the two copies of $!A$ in the conclusion of $\pi'$ and $\type (\Gamma) = (\vec v; \vec x)$. 
										%		(Recall that the typing corresponding to $!$ means that all inputs for each $!A$ are normal). 
												We define $\vec f^\pi$ by duplicating the arguments for $!A$:
												\[
												\vec f^\pi (\vec u , \vec v ; \vec x)
												\quad := \quad
												\vec f' (\vec u, \vec u , \vec v ; \vec x)
												\]
												
												

%														\begin{proof}
%															[Proof of Thm.~\ref{thm:main-result}]
%															%		[Proof sketch]
%															By Thm.~\ref{thm:free-cut-elim} and Lemma~\ref{lemma:spec-norm-form} we have a free-cut free proof $\pi$ in $\closure{\eqspec} \cup \arith$ of $!\word (\vec x ) \seqar \word (f (\vec x))$. By Lemma~\ref{lemma:witness-invariant} above this means that $\vec a = \vec x \cimp f^\pi (\vec a) = f(\vec x)$ is true in any model of $\qfindth$ satisfying $\eqspec$ and $\eqspec^\pi$. 
%															%		Since some model must exist by coherence (cf.\ Prop.~\ref{prop:eq-spec-model}), we have that 
%															Using the fact that $\eqspec \cup \eqspec^\pi$ is coherent we can construct such a model, similarly to Prop.~\ref{prop:eq-spec-model}, which will contain $\Word$ as an initial segment, in which we must have $f^\pi (\vec x) = f (\vec x)$ for every $\vec x \in \Word$, as required.\todo{polish}
%														\end{proof}