The proof of those catch-up lemmas is very similar to the previous one for structural precision, but this time without the need for induction---we use \cref{lem:catchup-univ} instead. We show the one for product types, the others are identical.

First, let us show the property for $\capre$. Decompose $\tcol{T'}$ into $\tcol{\cast{U_{n-1}}{S_n}{\dots \cast{U_1}{S_2}{T''}}}$, where $\tcol{T''}$ is not a cast, but either some $\tcol{\?_{S}}$ or a product type structurally less precise than $\tcol{\P x : A.B}$. Now by \cref{lem:catchup-univ}, $\tcol{U_k}$, $\tcol{T_k}$ and possibly $\tcol{S}$ all reduce to $\tcol{[]}$ or $\tcol{\?_{[]}}$. Using the same reduction rules as before, all casts can be reduced away, leaving us with either $\tcol{\?_{[]}}$ or a product type structurally less precise than $\tcol{\P x : A.B}$, as stated.

\end{proof}

\begin{proof}[Proof of \cref{lem:catchup-lambda}]
The proof still follows the same idea: decompose the less precise term as a series of casts, and show that all those casts can be reduced, using \cref{lem:catchup-type} for product types. However it is somewhat more complex, because the reduction of a cast between product types does a substitution, which we need to handle using the previous substitution lemma for precision.

Let us now detail the reasoning. First, decompose $\tcol{s'}$ into $\tcol{\cast{U_{n-1}}{S_n}{\dots \cast{U_1}{S_2}{u'}}}$, where $\tcol{u'}$ is either $\tcol{\l x : A''. t''}$ or $\tcol{\?_{S}}$ for some $\tcol{S}$. All of the $\tcol{S_k}$, $\tcol{U_k}$ and possibly $\tcol{S}$ are definitionally less precise than $\tcol{\P x : A. B}$. By definition of $\cdpre$ they all reduce to a term structurally less precise than a reduct of $\tcol{\P x : A . B}$, which must be a product type, and thus by \cref{lem:catchup-type} they all reduce to either some $\tcol{?_{[]_{j}}}$ or some product type. Moreover, given the typing hypothesis and confluence $\tcol{S_n}$ can only be in the second case. By rule \nameref{redrule:down-unk}, we get
\[\tcol{\cast{?_{[]}}{X}{?_{?_{[]}}} \redCCIC ?_{X}}\]
so if $\tcol{S}$ is $\tcol{\?_{[]}}$ we can reduce the innermost casts until it is (knowing that we will encounter one because $\tcol{S_n}$ is a product type), then use rule \nameref{redrule:prod-unk} on $\tcol{u'}$ if it applies, so that without loss of generality we can suppose that $\tcol{u'}$ is an abstraction.

Now we show that all casts reduce, and that this reduction preserves precision, starting with the innermost one. There are three possibilities for that innermost cast.

If it is $\tcol{\cast{\stalkCIC{j}{\Pi}}{?_{[]_j}}{u'}}$, then by typing this cannot be the outermost cast, and thus rule \nameref{redrule:up-down} applies to get
\[\tcol{ \cast{\?_{[]_j}}{X}{\cast{\stalkCIC{j}{\Pi}}{\?_{[]_j}}{u'}} \redCCIC \cast{\stalkCIC{j}{\Pi}}{X}{u'} }\]

In the second case, the cast is some $\tcol{\cast{\P x : A_1. B_1}{\P x : A_2. B_2}{\l x : A''. t''}}$, and rule \nameref{redrule:prod-prod} applies to give
\[\begin{array}{r}
\tcol{\cast{\P x : A_1. B_1}{\P x : A_2. B_2}{\l x :
A''. t''}} \redCCIC \hspace{12em}  \\ \tcol{\l x : A''
. \cast{B_1\subs{\cast{A_2}{A_1}{x}}{x}}{B_2}{t''\subs{\cast{A_2}{A''}{x}}{x}}} \end{array}\]
Moreover, using the precision hypothesis of \nameref{infrule:capre-castr}, we know that $\tcol{\GG} \vdash \tcol{\P x : A . B} \cdpre \tcol{\P x : A_1 . B_2}$ and $\tcol{\GG} \vdash \tcol{\P x : A . B} \cdpre \tcol{\P x : A_2 . B_2}$. From the first one, using substitution and rule \nameref{infrule:capre-castr}, we get that $\tcol{\GG, x : A \mid A_2} \vdash \tcol{B} \cdpre \tcol{B_1\subs{\cast{A_2}{A_1}{x}}{x}}$.
The second gives in particular that $\tcol{\GG} \vdash \tcol{A} \cdpre \tcol{A_2}$. Finally, inverting the proof of $\tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{\l x : A'' . t''}$ we also have $\tcol{\GG} \vdash \tcol{A} \capre \tcol{A''}$ and $\tcol{\GG, x : A \mid A''} \vdash \tcol{t} \capre \tcol{t''}$. From this, again by substitution, we can derive $\tcol{\GG, x : A \mid A''} \vdash \tcol{t} \capre \tcol{t''\subs{\cast{A_2}{A''}{x}}{x}}$. Combining all of those, we can construct a derivation of
\[ \tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{\l x : A_2 . \cast{B_1\subs{\cast{A_2}{A_1}{x}}{x}}{B_2}{t'\subs{\cast{A_2}{A''}{x}}{x}}} \]
by a use of \nameref{infrule:capre-abs} followed by one of \nameref{infrule:capre-castr}.

The last case corresponds to $\tcol{\cast{\P x : A'' . B''}{?_{[]_j}}{u'}}$ when $\tcol{\P x : A'' . B''}$ is not $\tcol{\stalkCIC{j}{h}}$, in which case the reduction that applies is \nameref{redrule:prod-germ}, giving
\[\tcol{\cast{\P x : A'' . B''}{?_{[]_j}}{u'}} \redCCIC
\tcol{\cast{\?_{[]_{\castOfPi{j}}} \to \?_{[]_{\castOfPi{j}}}}{?_{[]_j}}{\cast{\P x : A'' . B''}{\?_{[]_{\castOfPi{j}}} \to \?_{[]_{\castOfPi{j}}}}{u'}}}\]
For this reduct to be less precise that $\tcol{\l x : A. t}$, we need that all types involved in the casts are definitionally precise than $\tcol{\P  x : A . B}$, as we already have that $\tcol{\GG} \vdash \tcol{\l x : A . t } \capre \tcol{u'}$. For $\tcol{\?_{[]_j}}$ and $\tcol{\P x : A''. B''}$ it is direct, as they were obtained using \cref{lem:catchup-type} with a reduct of $\tcol{\P x : A . B}$.
Thus only the germ remains, for which it suffices to show that both $\tcol{A}$ and $\tcol{B}$ are less precise than $\tcol{?_{[]_{\castOfPi{j}}}}$. Because $\tcol{\P x : A. B}$ is typable and less precise than $\tcol{\?_{[]_j}}$, we know that $\tcol{\fs{\GG}} \vdash \tcol{A} \pcheckty{[]} \tcol{[]_k}$ and $\tcol{\fs{\GG}, x : A} \vdash \tcol{B} \pcheckty{[]} \tcol{[]_l}$ with $\sortOfPi{k}{l} \leq j$, thus $k \leq \castOfPi{j}$ and $l \leq \castOfPi{j}$. Therefore $\tcol{\GG} \vdash \tcol{A} \capre \tcol{\?_{[]_{\castOfPi{j}}}}$ using rule \nameref{infrule:capre-unk-univ}, and similarly for $\tcol{B}$.

Note that this last reduction is the point where the system under consideration plays a role: in \CCICT, the reasoning does not hold. However, when considering only terms without $\tcol{\?}$, this case never happens, and thus the rest of the proof still applies.

Thus, all casts must reduce, and each of those reductions preserves precision, so we end up with a term $\tcol{\l x : A' . t'}$ such that $\tcol{\GG} \vdash \tcol{\l x : A . t} \capre \tcol{\l x : A' . t'}$, as expected.
\end{proof}

%\begin{lemma}[Constructors and inductive error catch-up]
%	\label{lem:pre-constructor}
%	If $\tcol{\GG} \vdash \tcol{c(\orr{a},\orr{b})} \capre \tcol{s'}$, $\tcol{\fs{\GG}} \vdash \tcol{c(\orr{a},\orr{b})} \inferty \tcol{I(\orr{a})}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})}$, then either $\tcol{s'} \rtred \tcol{\?_{I(\orr{a'})}}$ or $\tcol{s'} \rtred \tcol{c(\orr{a'},\orr{b'})}$ with $\tcol{\GG} \vdash \tcol{c(\orr{a},\orr{b})} \capre \tcol{c(\orr{a'},\orr{b'})}$.
%	Similarly, if $\tcol{\GG} \vdash \tcol{\?_{I(\orr{a})}} \capre \tcol{s'}$, $\tcol{\fs{\GG}} \vdash \tcol{\?_{I(\orr{a})}} \inferty \tcol{I(\orr{a})}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})}$, then $\tcol{s'} \rtred \tcol{\?_{I(\orr{a'})}}$ with $\tcol{\GG} \vdash \tcol{I(\orr{a})} \capre \tcol{I(\orr{a'})}$.

\begin{proof}[Proof of \cref{lem:catchup-cons}]
We start by the proof of the second property. We have as hypothesis that $\tcol{\GG} \vdash \tcol{\?_{I(\orr{a})}} \capre \tcol{s'}$, $\tcol{\fs{\GG}} \vdash \tcol{\?_{I(\orr{a})}} \inferty \tcol{I(\orr{a})}$ and $\tcol{\sn{\GG}} \vdash \tcol{s'} \pcheckty{I} \tcol{I(\orr{a'})}$, and wish to prove that $\tcol{s'} \rtred \tcol{\?_{I(\orr{a'})}}$ with $\tcol{\GG} \vdash \tcol{I(\orr{a})} \capre \tcol{I(\orr{a'})}$.

As previously, decompose $\tcol{s'}$ as $\tcol{\cast{U_{n-1}}{S_n}{\dots \cast{U_1}{S_2}{\?_{I(\orr{a''})}}}}$, where all $\tcol{U_k}$, $\tcol{S_k}$ and $\tcol{I(\orr{a''})}$ are definitionally less precise than $\tcol{I(\orr{a})}$, and thus reduce to either $\tcol{\?_{[]_l}}$ for some $l$, or $\tcol{I(\orr{c})}$ for some $\tcol{\orr{c}}$, and $\tcol{S_n}$ can only be the second by typing. Using the three rules \nameref{redrule:ind-unk}, \nameref{redrule:up-down} and \nameref{redrule:ind-germ}, we respectively get
\begin{align*}
\tcol{\cast{I(\orr{c})}{I(\orr{c'})}{\?_{I(\mathbf{c''})}}}
&\redCCIC \tcol{\?_{I(\orr{c'})}} \\
\tcol{ \cast{\?_{[]_j}}{X}{\cast{\stalkCIC{j}{I}}{\?_{[]_j}}{u'}}}
&\redCCIC \tcol{\cast{\stalkCIC{j}{I}}{X}{u'}} \\
\tcol{\cast{I(\orr{c})}{\?_{[]_j}}{u'}}
& \redCCIC \tcol{\cast{\stalkCIC{j}{I}}{\?_{[]_j}}{\cast{I(\orr{c})}{\stalkCIC{j}{I}}{u'}}}
\end{align*}
we can reduce all casts: \nameref{redrule:up-down} (possibly using \cref{redrule:ind-germ} first) removes all casts through $\?_{[]}$; we can then use \nameref{redrule:ind-unk} to propagate $\?_{I(\orr{a''})}$ all the way through the casts, ending up with $\tcol{\?_{S_n}}$ which is the term we sought.

For the first property, again decompose $\tcol{s'}$ as $\tcol{\cast{U_{n-1}}{S_n}{\dots \cast{U_1}{S_2}{u'}}}$ where $\tcol{u'}$ does not start with a cast. If $\tcol{u'}$ is some $\tcol{\?_{I(\orr{a''})}}$, we can re-use the proof above and are finished. Otherwise $\tcol{u'}$ must be of the form $\tcol{c(\orr{a''},\orr{b''})}$. Again we reduce the casts starting with the innermost, using rules \nameref{redrule:up-down} and \nameref{redrule:ind-germ} to remove the occurrences of $\tcol{\?_{[]}}$. The last case to handle is $\tcol{\cast{I(\orr{c})}{I(\orr{c'})}{c(\orr{a_3},\orr{b_3})}}$. Then rule \nameref{redrule:ind-ind} applies, and it preserves precision by repeated uses of the substitution property, and giving a term with $\tcol{c}$ as a head constructor. Thus, we get the desired term with $\tcol{c}$ as a head constructor and arguments less precise than $\tcol{\orr{a}}$ and $\tcol{\orr{b}}$, respectively.
\end{proof}

\paragraph{Simulation}

% \begin{theorem}[Simulation of reduction]
% 	The two following properties are true:
% 	\begin{enumerate}
% 		\item if $\cdpre \tcol{\GG}$, $\tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{T}$, $\tcol{\sn{\GG}} \vdash \tcol{t'} \inferty \tcol{T'}$, $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ and $t \rtred s$ then there exists $\tcol{s'}$ such that $\tcol{t'} \rtred \tcol{s'}$ and $\tcol{\GG} \vdash \tcol{t'} \capre \tcol{s'}$,
% 		\item if $\cdpre \tcol{\GG}$, $\tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{T}$, $\tcol{\sn{\GG}} \vdash \tcol{t'} \inferty \tcol{T'}$, $\tcol{\GG} \vdash \tcol{t} \cdpre \tcol{t'}$ and $\tcol{t} \rtred \tcol{s}$ then $\tcol{\GG} \vdash \tcol{s} \cdpre \tcol{t'}$.
% 	\end{enumerate}
% \end{theorem}

\begin{proof}[Proof of \cref{thm:simulation}]
Both are shown by mutual induction on the precision derivation. We use a stronger induction principle that the one given by the induction rules. Indeed, we need extra induction hypothesis on the inferred type for a term. Proving this stronger principle is done by making the proof of \cref{prop:validity} slightly more general: instead of proving that an inferred type is always well-formed, we prove that any property consequence of typing is true of all inferred types. Let us now detail the most important cases of the inductive proof.

\paragraph{Definitional precision.}
We start with the easier second point. The proof is summarized by the following diagram:\\
\[\begin{tikzcd}[scale=0.6]
& \tcol{t} \arrow[dl] \arrow[d] & \cdpre &\tcol{t'} \arrow[d] \\
\tcol{s} \arrow[dr, dashed] & \tcol{u} \arrow[d, dashed] & \capre & \tcol{u'} \arrow[d, dashed] \\
& \tcol{v} & \capre & \tcol{v'}
\end{tikzcd}\]
By definition of $\cdpre$, there exists $\tcol{u}$ and $\tcol{u'}$, reducts respectively of $\tcol{t}$ and $\tcol{t'}$, and such that $\tcol{\GG} \vdash \tcol{u} \capre \tcol{u'}$. By confluence, there exists some $\tcol{v}$ that is a reduct of both $\tcol{u}$ and $\tcol{s}$. By subject reduction, $\tcol{u}$ and $\tcol{u'}$ are both well-typed, and thus by induction hypothesis there exists
$\tcol{v'}$ such that $\tcol{u'} \rtred \tcol{v'}$ and $\tcol{\GG} \vdash \tcol{v} \capre \tcol{v'}$. But then $\tcol{v}$ is a reduct of $\tcol{s}$ and $\tcol{v'}$ is a reduct of $\tcol{t'}$, and so $\tcol{\GG} \vdash \tcol{s} \cdpre \tcol{t'}$.

This implies in particular that if $\tcol{\GG} \vdash \tcol{t} \inferty \tcol{T}$, $\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}$, $\tcol{t} \rtred \tcol{s}$ and $\tcol{\fs{\GG}} \vdash \tcol{s} \inferty \tcol{S}$, then $\tcol{\GG} \vdash \tcol{S} \cdpre \tcol{T'}$. Indeed $\tcol{\fs{\GG}} \vdash \tcol{s} \checkty \tcol{T}$ by subject reduction, thus $\tcol{S}$ and $\tcol{T}$ are convertible, and have a common reduct $\tcol{U}$ by confluence.	The property just stated then gives $\tcol{\GG} \vdash \tcol{U} \cdpre \tcol{T'}$, hence $\tcol{\GG} \vdash \tcol{S} \cdpre \tcol{T'}$.

\paragraph{Syntactic precision---Non-diagonal precision rules.}
Let us now turn to $\capre$. It is enough to show that one step of reduction can be simulated, by induction on the path $\tcol{t} \rtred \tcol{s}$.

First, we get rid of most cases where the last rule used for $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ is not a diagonal rule.
For \nameref{infrule:capre-unk} we must handle the side-condition involving the type of $\tcol{t}$. However, by the previous property, the inferred type of $\tcol{s}$ is also definitionally less precise than $\tcol{T'}$. Thus the reduction in $\tcol{t}$ can be simulated by zero reduction steps. The reasoning for rules \nameref{infrule:capre-err} and \nameref{infrule:capre-err-lambda} is similar. As for rule \nameref{infrule:capre-univ}, subject reduction is enough to get what we seek, without even resorting to the previous property. Rule \nameref{infrule:capre-castr} is treated in the same way as \nameref{infrule:capre-unk}, as the typing side-conditions are similar.
Thus the only non-diagonal rule left for $\capre$ is \nameref{infrule:capre-castl}.

\paragraph{Syntactic precision---Non-top-level reduction.}

Next, we can get rid of reductions that do not happen at top level. Indeed, if the last rule used was \nameref{infrule:capre-castl}, and the reduction happens in one of the types of the cast, the same reasoning as for \nameref{infrule:capre-castr} applies. If it happens in the term, we can use the induction hypothesis on this term to conclude.
Also, if the last rule used was a diagonal rule, then the reduction in $\tcol{t}$ can be simulated by a similar congruence rules in $\tcol{t'}$.

So we are left with the simulation of a reduction that happens at the top-level in $\tcol{t}$, and where the last precision rule used is either \nameref{infrule:capre-castl} or a diagonal one, and this is the real core of the proof.

\paragraph{Syntactic precision---non-diagonal cast.}
Let us first turn to the case where the last precision rule is \nameref{infrule:capre-castl}, and that cast reduces. More precisely, $\tcol{t}$ is some $\tcol{\cast{S}{T}{u}}$, with $\tcol{\GG} \vdash \tcol{u} \capre \tcol{t'}$. There are four possibilities for the reduction.
\begin{itemize}

\item The cast fails. When it does, whatever the rule, it always reduces to $\tcol{\err_{T}}$. But then we know that $\tcol{\sn{\GG}} \vdash \tcol{t'} \inferty \tcol{T'}$ and $\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}$. Thus $\tcol{\GG} \vdash \tcol{\err_{T}} \capre \tcol{t'}$ by rule \nameref{infrule:capre-err}, and the reduction is simulated by zero reductions.

\item The cast disappears (\nameref{redrule:univ-univ}) or expands into two casts without changing $\tcol{u}$ (\nameref{redrule:ind-germ}, \nameref{redrule:prod-germ}). In those cases the reduct of $\tcol{t}$ is still smaller than $\tcol{t'}$. In the case of cast expansion, we must use \nameref{infrule:capre-castl} twice, and thus prove that the type of $\tcol{t'}$ is less precise than the introduced germ. But by the \nameref{infrule:capre-castl} rule that was used to prove $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$, we know that $\tcol{t'}$ infers a type $\tcol{T'}$ which is definitionally less precise than some $\tcol{\?_{[]_i}}$. Thus, $\tcol{T'}$ reduces to some $\tcol{S'}$ such that $\tcol{\GG} \vdash \tcol{\?_{[]_i}} \capre \tcol{S'}$, and this implies that also $\tcol{\GG} \vdash \tcol{\stalkCIC{i}{h}} \capre \tcol{S'}$, \ie what we sought.

\item Both $\tcol{T}$ and $\tcol{S}$ are either product types or inductive types, and $\tcol{u}$ starts with an abstraction or an inductive constructor. In that case, by \cref{lem:catchup-lambda,lem:catchup-cons}, $\tcol{t'}$ reduces to a term $\tcol{u'}$ with the same head constructor as $\tcol{u}$
or some $\tcol{\?_{I(\orr{a})}}$. In the first case, by the substitution property of precision we have $\tcol{\GG} \vdash \tcol{s} \capre \tcol{u'}$. In the second, we can use \nameref{infrule:capre-unk} to conclude.

\item The reduction rule is \nameref{redrule:up-down}, that is $\tcol{t}$ is $\tcol{\cast{?_{[]_i}}{T}{\cast{\stalkCIC{i}{h}}{\?_{[]_i}}{u}}}$ which reduces to $\tcol{\cast{\stalkCIC{i}{h}}{T}{u}}$.
If rule \nameref{infrule:capre-castl} was used twice in a row then we directly have $\tcol{\GG} \vdash \tcol{u} \capre \tcol{t'}$ and so $\tcol{\GG} \vdash \tcol{\cast{\stalkCIC{i}{h}}{X}{u}} \capre \tcol{t'}$. Otherwise, rule \nameref{infrule:capre-diag-cast} was used, $\tcol{t'}$ is some $\tcol{\cast{S'}{T'}{u'}}$ and we have $\tcol{\GG} \vdash \tcol{u} \capre \tcol{u'}$ and $\tcol{\fs{\GG}} \vdash \tcol{\stalkCIC{i}{h}} \cdpre \tcol{S'}$.
Moreover, \nameref{infrule:capre-castl} also gives $\tcol{\fs{\GG}} \vdash \tcol{X} \cdpre \tcol{B'}$, since $\tcol{\sn{\GG}} \vdash \tcol{\cast{A'}{B'}{u'}} \inferty \tcol{B'}$. Thus $\tcol{\GG} \vdash \tcol{\cast{\stalkCIC{i}{h}}{X}{u}} \capre \tcol{\cast{A'}{B'}{u'}}$ by a use of \nameref{infrule:capre-diag-cast}.

\end{itemize}

\paragraph{Syntactic precision---$\beta$ redex.}
Next we consider the case where $\tcol{t}$ is a $\beta$ redex $\tcol{(\l x : A . t_1)~t_2}$. Because the last applied precision rule is diagonal, $\tcol{t'}$ must also decompose as $\tcol{t_1''~t_2'}$. If $\tcol{t_1}$ is some $\tcol{\err_{T}}$, then the reduct is $\tcol{\err_{T}}$ and must be still smaller that $\tcol{t'}$. Otherwise, \cref{lem:catchup-lambda} applies, thus $\tcol{t_1''}$ reduces to some $\tcol{\l x : A' . t_1'}$ that is syntactically less precise than $\tcol{\l x : A . t_1}$. Then the $\beta$ reduction of $t$ can be simulated with a $\beta$ reduction in $\tcol{t'}$, and using the substitution property we conclude that the redexes are still related by precision.

\paragraph{Syntactic precision---$\iota$ redex.}
If $\tcol{t}$ is a $\iota$ redex $\tcol{\match{c(\orr{a},\orr{b})}{I}{z.P}{\orr{f.\orr{y}.t}}}$, the reasoning is similar. Because the last precision rule is diagonal, $\tcol{t'}$ must also be a fixpoint. We thus can use \cref{lem:catchup-cons} to ensure that its scrutinee reduces either to $\tcol{c(\orr{a'},\orr{b'})}$ or $\tcol{\?_{I(\orr{a'})}}$. In the first case, a $\iota$ reduction of $\tcol{t'}$ and the substitution property is enough to conclude.
In the second case, $\tcol{t'}$ reduces to a term $\tcol{s'} := \tcol{\?_{P'\subs{\?_{I(\orr{a'})}}{z}}}$, and we must show this term to be less precise than $\tcol{s}$, which is $\tcol{t_k\subs{\l x : I(\orr{a}) . \match{I}{x}{z.P}{\orr{f.\orr{y}.t}}}{z}\subs{\orr{b}}{\orr{y}}}$.
Let $\tcol{S}$ be the type inferred for $\tcol{s}$, by rule \nameref{infrule:capre-unk}, it is enough to show $\tcol{\GG} \vdash \tcol{S} \cdpre \tcol{P'\subs{\?_{I(\orr{a'})}}{z}}$. By subject reduction, $\tcol{S}$ and $\tcol{P\subs{c_k(\orr{a},\orr{b})}{z}}$ (the type of $\tcol{t}$) are convertible, thus they have a common reduct $\tcol{U}$. Now we also have by substitution that $\tcol{\GG} \vdash \tcol{P\subs{c_k(\orr{a},\orr{b})}{z}} \capre \tcol{P'\subs{\?_{I(\orr{a'})}}{z}}$. Because $\tcol{P\subs{c_k(\orr{a},\orr{b})}{z}}$ is the inferred type for $\tcol{t}$, the induction hypothesis applies to it, and thus there is some $\tcol{U'}$ such that $\tcol{P'\subs{\?_{I(\orr{a'})}{z}}} \rtred \tcol{U'}$ and also $\tcol{\GG} \vdash \tcol{U} \capre \tcol{U'}$.

\paragraph{Syntactic precision---$\err$ and $\?$ reductions.}
For reductions \nameref{redrule:prod-err}, \ie when $\tcol{\err_{\P x : A.B}} \redCCIC \tcol{\l x : A . \err_B}$, we can replace the use of \nameref{infrule:capre-err} by a use of \nameref{infrule:capre-err-lambda}. For reduction \nameref{redrule:ind-err}, \ie when $\tcol{t}$ is $\tcol{\match{I}{\err_{I(\orr{a})}}{z.P}{\orr{f.y.t}}}$ we distinguish three cases depending on $\tcol{t'}$. If $\tcol{t'}$ is $\tcol{\?_{T'}}$ (the precision rule between $\tcol{t}$ and $\tcol{t'}$ was \nameref{infrule:capre-unk}) or $\tcol{\cast{S'}{T'}{t'}}$, then $\tcol{\GG} \vdash \tcol{P\subs{\err_{I(\orr{a})}}{z} \cdpre T'}$, and thus $\tcol{\GG} \vdash \tcol{\err_{P\subs{\err{_{I(\orr{a})}}}{z}}} \capre \tcol{t'}$ by using \nameref{infrule:capre-err}. Otherwise, the last rule was \nameref{infrule:capre-fix}, and again we can conclude using \nameref{infrule:capre-err} and the substitution property of $\capre$.

Conversely, let us consider the reduction rules for $\tcol{\?}$. If $\tcol{t}$ is $\tcol{\?_{\P x : A.B}}$ and reduces to $\tcol{\l x : A. \?_{B}}$, then $\tcol{t'}$ must be $\tcol{\?_{T}}$, possibly surrounded by casts.
If there are casts, they can all be reduced away until we are left with $\tcol{\?_{T'}}$ for some $\tcol{T'}$ such that $\tcol{\GG} \vdash \tcol{\P x : A. B} \cdpre \tcol{T}$. By \cref{lem:catchup-type}, $\tcol{T} \rtred \tcol{\?_{\?_{[]}}}$ or $\tcol{T} \rtred \tcol{T_{\P x : A'. B'}}$. In the first case, $\tcol{\?_{\?_{[]}}}$ is still less precise than $\tcol{\l x : A. B}$, and in the second case, $\tcol{\?_{\P x : A'. B'}}$ can reduce to $\tcol{\l x : A' . \?_{B'}}$, which is less precise than $\tcol{s'}$.
If $\tcol{t}$ is $\tcol{\match{I}{\?_{I(\orr{a})}}{P}{\orr{b}}}$, reducing to $\tcol{\?_{P\subs{\?_{I(\orr(a))}}{z}}}$, we use the second part of \cref{lem:catchup-cons} to conclude that also $\tcol{t'}$ reduces to some $\tcol{\match{I}{\?_{I(\orr{a'})}}{P'}{\orr{b'}}}$ that is less precise than $\tcol{t}$. From this, $\tcol{t'} \redCCIC \tcol{\?_{P'\subs{\?_{I(\orr(a'))}}{z}}}$, which is less precise than $\tcol{s}$.

\paragraph{Syntactic precision---diagonal cast reduction.}
This only leaves us with the reduction of a cast when the precision rule is \nameref{infrule:capre-diag-cast}: we have some $\tcol{\cast{S}{T}{u}}$ and $\tcol{\cast{S'}{T'}{u'}}$ that are pointwise related by precision, such that $\tcol{\cast{S}{T}{t}} \rtred \tcol{s}$ by a head reduction, and we must show that $\tcol{\cast{S}{T}{u}}$ simulates that reduction.

First, if the reduction for $\tcol{\cast{S}{T}{t}}$ is any reduction to an error, then the reduct is $\tcol{\err_{T}}$, and since $\tcol{\sn{\GG}} \vdash \tcol{\cast{S'}{T'}{u'}} \inferty \tcol{T'}$ and $\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}$ we can use rule \nameref{infrule:capre-err} to conclude.

Next, consider \nameref{redrule:prod-prod}. We are in the situation where $\tcol{t}$ is $\tcol{\cast{\P x : A_1 . B_1}{\P x : A_2.B_2}{\l x : A. v}}$.
If $\tcol{v}$ is $\tcol{\err_{B_1}}$ then the reduct is more precise than any term.
Otherwise, by \cref{lem:catchup-type}, $\tcol{S'}$ reduces either to $\tcol{\?_{[]}}$ or to a product type. In the first case, $\tcol{u'}$ must reduce to $\tcol{\?_{\?_{[]}}}$ by \cref{lem:catchup-lambda}, since it is less precise than $\tcol{\l x : A.v}$ and by typing it cannot start with a $\tcol{\lambda}$. In that case, $\tcol{\cast{S'}{T'}{u'}} \redCCIC \tcol{\?_{T'}}$, and since $\tcol{\GG} \vdash \tcol{\P x : A_2. B_2} \cdpre \tcol{T'}$, we have that $\tcol{\GG} \vdash \tcol{s} \capre \tcol{\?_{T'}}$.
Otherwise $\tcol{S'}$ reduces to some $\tcol{\P x : A_1'. B_1'}$. By \cref{lem:catchup-lambda}, $\tcol{t'}$ reduces either to some $\tcol{\?}$ or to an abstraction. In the first case, the previous reasoning still applies. Otherwise, $\tcol{t'}$ reduces to some $\tcol{\l x : A' . v'}$. Again, by \cref{lem:catchup-type}, $\tcol{T'}$ reduces either to a product type or to $\tcol{\?}$.
In the first case $\tcol{t'}$ can simply do the same cast reduction as $\tcol{t}$, and the substitution property of precision enables us to conclude. Thus, the only case left is that where $\tcol{t'}$ is $\tcol{\cast{\P x : A_1'. B_1'}{\?_{[]_i}}{\l x : A' . v'}}$. If $\tcol{\P x : A_1' . B_1'}$ is $\tcol{\stalkCIC{i}{\P}}$, then all of $\tcol{A}$, $\tcol{A_1}$, $\tcol{A_2}$, $\tcol{B_1}$ and $\tcol{B_2}$ are more precise than $\tcol{\?_{[]_{\castOfPi{i}}}}$, and this is enough to conclude that $\tcol{s}$ is less precise than $\tcol{\cast{\?_{[]_i}}{\stalkCIC{i}{\P}}{\l x : ?_{[]_{\castOfPi{i}}}.u'}}$, using the substitution property of precision to relate $\tcol{u'}$ with the substituted $\tcol{u}$, and the \nameref{infrule:capre-abs}, \nameref{infrule:capre-castl} and \nameref{infrule:capre-castr} rules.
The last case is when $\tcol{\P x : A_1' . B_1'}$ is not a germ. Then the reduction of $\tcol{t'}$ first does a cast expansion through $\tcol{\stalkCIC{i}{\Pi}}$, followed by a reduction of the cast between $\tcol{\P x : A_1' . B_1'}$ and $\tcol{\stalkCIC{i}{\Pi}}$. The reasoning of the two previous cases can be used again to conclude.
The proof is similar for rule \nameref{redrule:ind-ind}.

Next, let us consider \nameref{redrule:prod-germ}, that is when $\tcol{t}$ is $\tcol{\cast{\P x : A_1 . B_1}{\?_{[]_i}}{f}}$. We have that $\tcol{T' \redCCIC \?_{[]_j}}$ by \cref{lem:catchup-type} with $i \leq j$, and thus $\tcol{\GG} \vdash \tcol{\stalkCIC{i}{\Pi}} \cdpre \tcol{T'}$. Thus, using \nameref{infrule:capre-diag-cast} for the innermost cast in $\tcol{s}$, and \nameref{infrule:capre-castl} for the outermost one, we conclude $\tcol{\GG} \vdash \tcol{s} \capre \tcol{\cast{S'}{T'}{u'}}$. Again, the reasoning is similar for \nameref{redrule:ind-germ}.

As for \nameref{redrule:univ-univ}, $\tcol{t}$ is $\tcol{\cast{[]_i}{[]_i}{A}}$, and we can replace rule \nameref{infrule:capre-diag-cast} by rule \nameref{infrule:capre-castr}. Indeed $\tcol{\fs{\GG}} \vdash \tcol{A} \checkty \tcol{[]_i}$ by typing, thus $\tcol{\fs{\GG}} \vdash \tcol{A} \inferty \tcol{T}$ for some $\tcol{T}$ such that $\tcol{T} \redCCIC \tcol{[]_i}$. Therefore, since $\tcol{\GG} \vdash \tcol{[]_i} \cdpre \tcol{T'}$, we have $\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{T'}$ and similarly $\tcol{\GG} \vdash \tcol{T} \cdpre \tcol{S'}$. Thus, rule \nameref{infrule:capre-castr} gives $\tcol{\GG} \vdash \tcol{A} \capre \tcol{t'}$.

The last case left is the one of \nameref{redrule:up-down}, where $\tcol{t}$ is $\tcol{\cast{\?_{[]_i}}{X}{\cast{\stalkCIC{i}{h}}{\?_{[]_i}}{v}}}$. We distinguish on the rule used to prove $\tcol{\GG} \vdash \tcol{\cast{\stalkCIC{i}{h}}{\?_{[]_i}}{v}} \capre \tcol{u'}$. If it is \nameref{infrule:capre-castl}, then we simply have $\tcol{\GG} \vdash \tcol{\cast{\stalkCIC{i}{h}}{X}{t}} \capre \tcol{\cast{S'}{T'}{u'}}$ using rule \nameref{infrule:capre-diag-cast}, as $\tcol{\GG} \vdash \tcol{\stalkCIC{i}{h}} \cdpre \tcol{S'}$ since $\tcol{\GG} \vdash \tcol{\?_{[]_i}} \cdpre \tcol{S'}$. Otherwise the rule is \nameref{infrule:capre-diag-cast}, $\tcol{t'}$ reduces to $\tcol{\cast{\?_{[]_j}}{T'}{\cast{U'}{\?_{[]_j}}{u'}}}$, using \cref{lem:catchup-type} to reduce types less precise than $\tcol{\?_{[]_i}}$ to some $\tcol{\?_{[]_j}}$ with $i \leq j$. We can use \nameref{infrule:capre-diag-cast} on the outermost cast, and \nameref{infrule:capre-castr} on the innermost to prove that this term is less precise than $\tcol{s}$, as $\tcol{\GG} \vdash \tcol{\stalkCIC{i}{h}} \cdpre \tcol{\?_{[]_j}}$ since $i \leq j$.
\end{proof}

%\begin{corollary}[Reduction and types]
%	\label{cor:red-types-long}
%	If $\fs{\GG} \vdash \tcol{T}  \pcheckty{[]} \tcol{\square{}_i}$, $\sn{\GG} \vdash \tcol{T'} \pcheckty{[]} \tcol{\square{}_j}$, $\GG \vdash \tcol{T} \capre \tcol{T'}$ then
%	\begin{itemize}
%		\item if $\tcol{T} \rtred \tcol{\?_{[]_j}}$ then $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ with $i \leq j$;
%		\item if $\tcol{T} \rtred \tcol{\square{}_{i-1}}$ then either $\tcol{T'} \rtred \tcol{\?_{\square{}_j}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{\square{}_{i-1}}$;
%		\item if $\tcol{T} \rtred \tcol{\P x : A. B}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_j}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{\P x : A'. B'}$ and $\GG \vdash \tcol{\P x : A.B} \capre \tcol{\P x : A'.B'}$;
%		\item if $\tcol{T} \rtred \tcol{I(\orr{a})}$ then either $\tcol{T'} \rtred \tcol{\?_{[]_i}}$ with $i \leq j$, or $\tcol{T'} \rtred \tcol{I(\orr{a'})}$ and $\GG \vdash \tcol{I(\orr{a})} \capre \tcol{I(\orr{a'})}$.
%	\end{itemize}

\subsection{Properties of \GCIC}
\label{sec:properties-gcic}

Conservativity is an equivalence, so to prove it we break it down into two implications. We now state and prove those in an open context and for the three different judgments.

\begin{theorem}[\GCIC is weaker than \CIC---Open context]~
Let $\scol{\tilde{t}}$ be a static term and $\tcol{\Gamma}$ an erasable context. Then
\begin{itemize}
\item if $\eras(\tcol{\Gamma}) \cicty \tcol{t} \inferty T$ then $\inferelab{}{\tilde{t}}{}{\Gamma}{t}{T'}$ for some erasable $\tcol{t}$ and $\tcol{T'}$ such that $\eras(\tcol{t}) = \scol{\tilde{t}}$ and $\eras(\tcol{T'}) = T$;
\item if $\tcol{T'}$ is an erasable term of \CCIC, and $\eras(\tcol{\Gamma}) \cicty \scol{\tilde{t}} \checkty \eras(\tcol{T'})$ then $\checkelab{}{\tilde{t}}{}{\Gamma}{t}{T'}$ for some erasable $\tcol{t}$ such that $\eras(\tcol{t}) = \scol{\tilde{t}}$;
\item if $\eras(\tcol{\Gamma}) \cicty \scol{\tilde{t}} \pcheckty{h} T$ then $\pcheckelab{h}{}{\tilde{t}}{}{\Gamma}{t}{T'}$ for some erasable $\tcol{t}$ and $\tcol{T'}$ such that $\eras(\tcol{t}) = \scol{\tilde{t}}$ and $\eras(\tcol{T'}) = T$.
\end{itemize}
\end{theorem}

\begin{proof}
Once again, the proof is by mutual induction, on the typing derivation of $\scol{\tilde{t}}$ in \CIC.

All inference rules are direct: one needs to combine the induction hypothesis together, using the substitution property of precision and the fact that erasure commutes with substitution to handle the cases of substitution in the inferred types.

Let us consider the case of \nameref{infrule:cic-prod-inf} next. We are given $\tcol{\Gamma}$ erasable, and suppose $\eras(\tcol{\Gamma}) \cicty \scol{\tilde{t}} \inferty T$ and $T \rtred \P x : A .B$. By induction hypothesis there exists $\tcol{t}$ and $\tcol{T'}$ erasable such that $\inferelab{}{\ccol{t}}{}{\Gamma}{\scol{\tilde{t}}}{T'}$ and $\eras(\tcol{t}) = \scol{\tilde{t}}$, $\eras(\tcol{T'}) = T$. Because $\tcol{T'}$ is erasable, it is less precise than $T$. By \cref{cor:red-types}, it must reduce to either $\tcol{\?_{[]}}$ or a product type. The first case is impossible because $\tcol{T'}$ does not contain any $\tcol{\?}$ as it is erasable. Thus there are some $\tcol{A'}$ and $\tcol{B'}$ such that $\tcol{T'} \rtred \tcol{\P x : A' . B'}$ and $\tcol{\Gamma} \vdash \P x : A.B \capre \tcol{\P x : A'. B'}$. Since also $\tcol{\Gamma} \vdash \tcol{T'} \capre T$, by the same reasoning there are also some $A''$ and $B''$ such that $T \rtred \P x : A''. B''$ and $\tcol{\Gamma} \vdash \tcol{\P x : A' . B'} \capre \P x : A'' . B''$. Now because $T$ is static, so are $\P x : A . B$ and $\P x : A''. B''$, and because of the comparisons with $\P x : A' . B'$ we must have $\eras(\Gamma) \vdash \P x : A . B \capre \P x : A'' . B''$. Since both are static, this means they must be $\alpha$-equal, since no non-diagonal rule can be used on static terms. Hence, $\P x : A . B = \P x : A'' . B'' = \eras(\tcol{\P x : A'. B '})$, implying that $\tcol{\P x : A' . B'}$ is erasable.
Thus, $\pcheckelab{\Pi}{}{\tilde{t}}{}{\Gamma}{t}{\P x : A'.B'}$, both $\tcol{t}$ and $\tcol{\P x : A' . B'}$ are erasable, and moreover $\eras(\tcol{t}) = \scol{\tilde{t}}$ and $\eras(\tcol{\P x : A' . B'}) = \P x : A.B$, which is what had to be proven.

The other constrained inference rules being very similar, let us turn to \nameref{infrule:cic-check}. We are given $\tcol{\Gamma}$ and $\tcol{T'}$ erasable, and suppose that $\eras(\tcol{\Gamma}) \cicty \scol{\tilde{t}} \inferty S$ such that $S \conv \eras(\tcol{T'})$.
By induction hypothesis, $\inferelab{}{\tilde{t}}{}{\Gamma'}{t}{S'}$ with $\tcol{t}$ and $\tcol{S'}$ erasable, $\eras(\tcol{t}) = \scol{\tilde{t}}$ and $\eras(\tcol{S'}) = S$. But convertibility implies consistency, so $S \cons \eras(\tcol{T'})$.
By monotonicity of consistency, this implies $\tcol{S'} \cons \tcol{T'}$. Thus $\checkelab{}{\tilde{t}}{}{\Gamma}{\cast{S'}{T'}{t}}{T'}$. We have $\eras(\tcol{\cast{S'}{T'}{t}}) = \eras(\tcol{t}) = \scol{\tilde{t}}$, so we are left with showing that $\tcol{\Gamma} \vdash \tcol{\cast{S'}{T'}{t}} \caequipre \scol{\tilde{t}}$. Using rules \nameref{infrule:capre-castl} and \nameref{infrule:capre-castr}, and knowing already that $\tcol{\Gamma} \vdash \tcol{S'} \caequipre S$, it remains to show that $\tcol{\Gamma} \vdash \tcol{T'} \cdpre S$ and $\Gamma \vdash S \cdpre \tcol{T'}$. As $S$ and $\eras(\tcol{T'})$ are convertible, let $U$ be a common reduct. Using \cref{thm:simulation}, $\tcol{T'} \rtred \tcol{U'}$ with $\tcol{\Gamma} \vdash U \capre \tcol{U'}$. Simulating that reduction again, we get $\eras(\tcol{T'}) \rtred U''$ with $\tcol{\Gamma} \vdash U'' \capre \tcol{U'}$. As before, this implies $U = U'' = \eras(\tcol{U'})$. Thus, using the reduct $\tcol{U'}$ of $\tcol{T'}$ that is equiprecise with $\tcol{U}$, we can conclude $\tcol{\Gamma} \vdash S \cdpre \tcol{T'}$ and $\tcol{\Gamma} \vdash \tcol{T'} \cdpre S$.
\end{proof}

\begin{theorem}[\CIC is weaker than \GCIC---Open context]
Let $\scol{\tilde{t}}$ be a static term and $\tcol{\Gamma}$ an erasable context of \CCIC. Then
\begin{itemize}
\item if $\inferelab{}{\tilde{t}}{}{\Gamma}{t}{T}$, then $\tcol{t}$ and $\tcol{T}$ are erasable, $\eras(\tcol{t'}) = \scol{\tilde{t}}$ and $\eras(\tcol{\Gamma}) \vdash \scol{\tilde{t}} \inferty \eras(\tcol{T'})$;
\item if $\tcol{T'}$ is an erasable term of \CCIC such that $\checkelab{}{\tilde{t}}{}{\Gamma'}{t'}{T'}$, then $\tcol{t'}$ is erasable, $\eras(t') = \scol{\tilde{t}}$ and $\eras(\tcol{\Gamma}) \vdash \scol{\tilde{t}} \checkty \eras(\tcol{T'})$;
\item if $\pcheckelab{h}{}{\tilde{t}}{}{\Gamma'}{t'}{T'}$, then $\tcol{t'}$ and $\tcol{T'}$ are erasable, $\eras(\tcol{t'}) = \scol{\tilde{t}}$ and $\eras(\tcol{\Gamma}) \vdash \scol{\tilde{t}} \pcheckty{h} \eras(\tcol{T'})$.
\end{itemize}
\end{theorem}

\begin{proof}
The proof is similar to the previous one. Again, the tricky part is to handle reduction steps, and we use equiprecision in the same way to conclude in those.
\end{proof}

As a direct corollary of those propositions in an empty context, we get conservativity \cref{thm:conservativity}.

\paragraph{Elaboration graduality}

Now for the elaboration graduality: again, we state it in an open context for all three typing judgments.

\begin{theorem}[Elaboration graduality---Open context]
Let $\tcol{\GG}$ be a context such that $\tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, and $\scol{\tilde{t}}$ and $\scol{\tilde{t}'}$ be two \GCIC terms such that $\scol{\tilde{t}} \apre \scol{\tilde{t}'}$. Then
\begin{itemize}
\item if $\inferelab{}{\tilde{t}}{}{\fs{\GG}}{t}{T}$ is universe adequate, then there exists $\tcol{t'}$ and $\tcol{T'}$ such that $\inferelab{}{\tilde{t}'}{}{\sn{\GG}}{t'}{T'}$, $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ and $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$;
\item If $\checkelab{}{t}{}{\fs{\tcol{\GG}}}{t'}{T}$ is universe adequate, then for all $\tcol{T'}$ such that $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$ there exists $\tcol{t'}$ such that $\checkelab{}{\tilde{t}'}{}{\sn{\GG}}{t'}{T'}$ and $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$;
\item If $\pcheckelab{h}{}{t}{}{\fs{\tcol{\GG}}}{t'}{T}$ is universe adequate, then there exists $\tcol{t'}$ and $\tcol{T'}$ such that $\pcheckelab{h}{}{\tilde{t}'}{}{\sn{\GG}}{t'}{T'}$, $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ and $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$.
\end{itemize}
\end{theorem}

\begin{proof}
Once again, we use our favorite tool: induction on the typing derivation of $\scol{\tilde{t}}$.

\paragraph{Inference---Non-diagonal precision.}
For inference, we have to make a distinction on the rule used to prove $\scol{tilde{t}} \apre \scol{\tilde{t}'}$: we have to handle specifically the non-diagonal one, where $\scol{\tilde{t}'}$ is some $\scol{\?}$. We start with this, and treat the ones where the rule is diagonal (\ie when $\scol{\tilde{t}}$ and $\scol{\tilde{t}'}$ have the same head) next.

We have $\inferelab{}{\tilde{t}}{}{\fs{\GG}}{t'}{T'}$ and $\inferelab{}{\?\ulev{i}}{}{\sn{\GG}}{\?_{\?_{[]_i}}}{\?_{[]_i}}$. Correctness of elaboration gives $\tcol{\fs{\GG}} \vdash \tcol{t'} \inferty \tcol{T'}$, and by validity $\tcol{\fs{\Gamma}} \vdash \tcol{T'} \inferty \tcol{[]_i}$, universe adequacy ensuring us that this $i$ is the same as the one in $\scol{\tilde{t}'}$. Thus we have $\tcol{\GG} \vdash \tcol{T'} \capre \tcol{\?_{[]_i}}$ by rule \nameref{infrule:capre-unk}, and in turn $\tcol{\GG} \vdash \tcol{t'} \capre \tcol{\?_{\?_{[]_i}}}$ by a second use of the same rule, giving us the required conclusions.

\paragraph{Inference---Variable.}
Rule \nameref{infrule:gcic-var} gives us $(x : \tcol{T}) \in \tcol{\fs{\GG}}$. Because $\vdash \tcol{\fs{\GG}} \capre \tcol{\sn{\GG}}$, there exists some $\tcol{T'}$ such that $(x : \tcol{T'}) \in \tcol{\sn{\GG}}$, and $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$ using weakening. Thus, $\inferelab{}{x}{}{\sn{\GG}}{x}{T'}$, and of course $\tcol{\GG} \vdash \tcol{x} \capre \tcol{x}$.

%	\textbf{Inference---diagonal universe case}\\
%	By reflexivity.

\paragraph{Inference---Product.}
Premises of rule \nameref{infrule:gcic-prod} give $\pcheckelab{[]}{}{\tilde{A}}{}{\fs{\GG}}{A}{[]_i}$ and $\pcheckelab{[]}{}{\tilde{B}}{}{\fs{\GG}, x : A}{B}{[]_j}$, and the diagonal precision one gives $\scol{\tilde{A}} \apre \scol{\tilde{A}'}$ and $\scol{\tilde{B}} \apre \scol{\tilde{B}'}$. Applying the induction hypothesis, we get some $\tcol{A'}$ such that $\pcheckelab{[]}{}{\tilde{A}'}{}{\sn{\GG}}{A'}{[]_i}$ and $\tcol{\GG} \vdash \tcol{A} \capre \tcol{A'}$. The inferred type for $\scol{\tilde{A}'}$ must be $\tcol{[]_i}$ as it is some $\tcol{[]_j}$ because of the constrained elaboration, and it is less precise than $\scol{[]_i}$ by the induction hypothesis.
From this, we also deduce that $\tcol{\fs{\GG}, x : A} \capre \tcol{\sn{\GG}, x : A'}$. Hence the induction hypothesis can be applied to $\scol{\tilde{B}}$, giving $\pcheckelab{[]}{}{\tilde{B}'}{}{\sn{\GG}}{B'}{[]_j}$. Combining this with the elaboration for $\tcol{\tilde{A}'}$, we obtain $\inferelab{}{\P x : \tilde{A}'. \tilde{B}'}{}{\sn{\GG}}{\P x : A' . B'}{[]_{\sortOfPi{i}{j}}}$. Moreover, $\tcol{\GG} \vdash \tcol{\P x : A. B} \capre \tcol{\P x : A' . B'}$ by combining the precision hypothesis on $A$ and $B$, and also $\tcol{\GG} \vdash \tcol{[]_{\sortOfPi{i}{j}}} \capre \tcol{[]_{\sortOfPi{i}{j}}}$.

\paragraph{Inference---Application.}
From rule \nameref{infrule:gcic-app}, we have $\pcheckelab{\Pi}{}{\tilde{t}}{}{\fs{\GG}}{t}{\P x : A . B}$ and $\checkelab{}{\tilde{u}}{}{\fs{\GG}}{u}{A}$, and the diagonal precision gives $\scol{\tilde{t}} \apre \scol{\tilde{t}'}$ and $\scol{\tilde{u}} \apre \scol{\tilde{u}'}$. By induction, we have $\pcheckelab{\Pi}{}{\tilde{t}'}{}{\fs{\GG}}{t'}{\P x : A' . B'}$ for some $\tcol{t'}$, $\tcol{A'}$ and $\tcol{B'}$ such that $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$, $\tcol{\GG} \vdash \tcol{A} \capre \tcol{A'}$ and $\tcol{\GG, x : A \mid A'} \vdash \tcol{B} \capre \tcol{B'}$. Using the induction hypothesis again with that precision property on $\tcol{A}$ and $\tcol{A'}$ gives $\checkelab{}{\tilde{u}'}{}{\sn{\GG}}{u'}{A'}$ with $\tcol{\GG} \vdash \tcol{u} \capre \tcol{u'}$.
Therefore combining those we get $\inferelab{}{\tilde{t}'~\tilde{u}'}{}{\sn{\GG}}{t'~u'}{B'\subs{u'}{x}}$, $\tcol{\GG} \vdash \tcol{t~u} \capre \tcol{t'~u'}$ and, by substitution property of precision, $\tcol{\GG} \vdash \tcol{B\subs{u}{x}} \capre \tcol{B'\subs{u'}{x}}$.

\paragraph{Inference---Other diagonal cases.}
All other cases are similar to those: combining the induction hypothesis directly leads to the desired result, handling the binders in a similar way to that of products when needed.

\paragraph{Checking.}
For \nameref{infrule:gcic-check}, we have that $\inferelab{}{\tilde{t}}{}{\fs{\GG}}{t}{S}$, with $\tcol{S} \cons \tcol{T}$. By induction hypothesis, $\inferelab{}{\tilde{t}'}{}{\sn{\GG}}{\tilde{t}'}{S'}$ with $\tcol{\GG} \vdash \tcol{t} \capre \tcol{t'}$ and $\tcol{\GG} \vdash \tcol{S} \capre \tcol{S'}$. But we also have as an hypothesis that $\tcol{\GG} \vdash \tcol{T} \capre \tcol{T'}$. By monotonicity of consistency, we conclude that $\tcol{S'} \cons \tcol{T'}$, and thus $\checkelab{}{\tilde{t}'}{}{\sn{\GG}}{\cast{S'}{T'}{t'}}{T'}$. A use of \nameref{infrule:capre-diag-cast} then ensures that $\tcol{\GG} \vdash \tcol{\cast{S}{T}{t}} \capre \tcol{\cast{S'}{T'}{t'}}$, as desired.

\paragraph{Constrained inference---\nameref{infrule:gcic-inf-prod} rule.}
We are in the situation where $\inferelab{}{\tilde{t}}{}{\fs{\GG}}{t}{S}$ and $\tcol{S} \rtred \tcol{\P x : A. B}$. By induction hypothesis, $\inferelab{}{\tilde{t}'}{}{\sn{\GG}}{t'}{S'}$ with $\tcol{\GG} \vdash \tcol{S} \capre \tcol{S'}$. Using \cref{cor:red-types}, we get that $\tcol{S'} \rtred \tcol{\P x : A' . B'}$ such that $\tcol{\GG} \vdash \tcol{\P x : A . B} \capre \tcol{\P x : A' . B'}$, or $\tcol{S'} \rtred \tcol{\?_{[]_i}}$. In the first case, by rule \nameref{infrule:gcic-inf-prod} we get $\pcheckelab{\Pi}{}{\tilde{t}'}{}{\sn{\GG}}{t'}{\P x : A' . B'}$ together with the precision inequalities for $\tcol{t'}$ and $\tcol{\P x : A'. B'}$. In the second case, we can use rule \nameref{infrule:gcic-prod-unk} instead, and get $\pcheckelab{\Pi}{}{\tilde{t}'}{}{\sn{\GG}}{\cast{S'}{\stalkCIC{i}{\Pi}}{t'}}{\stalkCIC{i}{\Pi}}$, and $\castOfPi{i}$ is larger than the universe levels of both $\tcol{A'}$ and $\tcol{B'}$. A use of \nameref{infrule:capre-castr}, together with the fact that $\tcol{\GG} \vdash \tcol{A} \capre \tcol{\?_{[]_{\castOfPi{i}}}}$ by \nameref{infrule:capre-unk-univ} and similarly for $\tcol{B}$, gives that $\tcol{\GG} \vdash \tcol{t'} \capre \tcol{\cast{S'}{\stalkCIC{i}{\Pi}}{t'}}$, and the precision between types has been established already.

\paragraph{Constrained inference---\nameref{infrule:gcic-prod-unk}.}
This time, $\inferelab{}{\tilde{t}}{}{\fs{\GG}}{t}{S}$, but $\tcol{S} \rtred \tcol{\?_{[]_i}}$. By induction hypothesis, $\inferelab{}{\tilde{t}'}{}{\sn{\GG}}{t'}{S'}$ with $\tcol{\GG} \vdash \tcol{S} \capre \tcol{S'}$. By \cref{cor:red-types}, we get that $\tcol{S'} \rtred \tcol{\?_{[]_i}}$. Thus $\pcheckelab{\Pi}{}{\tilde{t}'}{}{\sn{\GG}}{\cast{S'}{\stalkCIC{i}{\Pi}}{t'}}{\stalkCIC{i}{\Pi}}$. A use of \nameref{infrule:capre-diag-cast} is enough to conclude.

\paragraph{Constrained inference---Other rules.}
All other cases are similar to the previous ones, albeit with a simpler handling of universe levels (since $\castOfPiName$ does not appear).

\end{proof}

\section{Connecting the discrete and monotone models}
\label{sec:logical-relation}

Comparing the discrete and the monotone translations, we can see that they
coincide on ground types such as $\nat$.
On functions over ground types, for instance $\nat {\to} \nat$, the
monotone interpretation is more conservative:
any monotone function $f : \monTy{\nat{\to}\nat}$ induces a function
$\tilde{f} : \bareTy{\nat{\to}\nat}$ by forgetting the monotonicity, but not all
functions from $\bareTy{\nat{\to}\nat}$ are monotone\footnote{For instance the
function swapping $\err_{ \liftNat{} }$ and $\?_{ \liftNat{} }$ is not monotone.}.

\begin{figure}[h]
\centering
\textbf{Translation of contexts}
\begin{align*}
\binlogrelTy{\cdot}\quad &:=\quad {\cdot}
&\binlogrelTy{\Gamma, x : A} \quad &{:=} \quad\binlogrelTy{\Gamma}, x_{\disc} : \bareTy{A}, x_{\mon} :
\monTy{A}, x_\binlrel : \binlogrelTy{A}~x_{\disc}~x_{\mon}
\end{align*}
\smallskip

\textbf{Logical relation on terms and types}

\[
\begin{array}[t]{lcl}
\binlogrelTy{A} & := & \El_\binlrel\,\binlogrelTm{A} \\[0.7em]
{\binlogrelTm{ x }} & := & x_\binlrel\\
{\binlogrelTm{\square{}_i}} & := & \uU_{\binlrel,i} \\
{\binlogrelTm{t~u}} & := & \binlogrelTm{t}~\bareTm{u}~\monTm{u}~\binlogrelTm{u}\\
{\binlogrelTm{\l x : A . t}} & := & \l (x_{\disc} : \bareTy{A}) (x_{\mon} : \monTy{A}) (x_\binlrel : \binlogrelTy{A}~x_{\disc}~x_{\mon}) . \binlogrelTm{t} \\
{\binlogrelTm{\P x : A . B}} & := & \PiU_\binlrel~\binlogrelTm{A}~(\l (x_{\disc} : \bareTy{A}) (x_{\mon} : \monTy{A}) (x_\binlrel : \binlogrelTy{A}~x_{\disc}~x_{\mon}). \binlogrelTy{ B }) \\
{\binlogrelTm{\nat}} & := & \natU_\binlrel \\
{\binlogrelTm{\?_A}} & := & \?_{\binlogrelTy{A}} : \binlogrelTy{A}~\?_{\bareTy{A}}~\?_{\monTm{A}}\\
{\binlogrelTm{\err_A}} & := & \err_{\binlogrelTy{A}} : \binlogrelTy{A}~\err_{\bareTy{A}}~\err_{\monTm{A}}\\
{\binlogrelTm{ \cas }} &:= & \cas_{\binlrel}
\end{array}
\]
\medskip

\begin{center}
\textbf{Inductive-recursive relational universe $\U_{\binlrel} :
\U^\disc{\to}\U^\mon{\to}\square$ }
\end{center}
\smallskip

\begin{mathpar}
\inferrule{A_\binlrel \in \U_{\binlrel, i}~A~A'\\
B \in \P(a : A)(a' : A'). \El_\binlrel\,A_\binlrel\,a\,a' \to \U_{\binlrel,j}\,(B\,a)~(B'\,a')}
{\PiU_\binlrel~A_\binlrel~B_\binlrel \in \U_{\binlrel,\sortOfPi{i}{j}}~(\PiU\,A\,B)~(\PiU{}\,A'\,B')} \and
\inferrule{j < i}{\uU_{\binlrel,j} \in \U_{\binlrel, i}~\uU_j~\uU_j} \and
\natU_\binlrel \in \U_{\binlrel,i}~\natU~\natU \and
\unkU[\binlrel] \in \U_{\binlrel,i}~\unkU~\unkU \and
\maltese_\binlrel \in \U_{\binlrel,i}~\maltese~\maltese
\end{mathpar}
\medskip
\begin{center}
\textbf{Decoding function $\El_\binlrel : \U_\binlrel\,A\,A' {\to} \El\,A {\to} \El\,A' {\to} \square{}$}
\end{center}
\smallskip
\begin{align*}
\El_\binlrel\,\uU_{\binlrel,j}~A~A' &:= \U_{\binlrel,j}~A~A'\\
\El_\binlrel\,\natU_\binlrel~n~m &:= n = m\\
\El_\binlrel\,\maltese_\binlrel~\unitK~\unitK &:= \unit\\
\El_\binlrel\,\unkU[\binlrel]~(c;x)~y &:= \El_\binlrel\,(\stalkCIC{\binlrel}{c})~x~(\texttt{downcast}_{\unkU, \stalkCIC{}{c}}\,y) \\ % (c, x) ~ y when x ~ downcast ? (ElC c) y
\El_\binlrel\,(\PiU_\binlrel~A_\binlrel~B_\binlrel)~f~f' &:= \P (a : \El\,A) (a' : \El\,A') (a_\binlrel : \El_\binlrel\,A_\binlrel~a~a').\\
\end{align*}
\caption{Logical relation between the discrete and monotone models}
\label{fig:logrel-discrete-monotone}
\end{figure}
Extending the sketched correspondence at higher types, we obtain a (binary)
logical relation $\binlogrelTm{-}$ between terms of the discrete and monotone
translations described in \cref{fig:logrel-discrete-monotone}, that forgets the
monotonicity information on ground types.
More precisely we define for each types $A$ in the source a relation
$\binlogrelTy{A} : \bareTy{A} \to \monTy{A} \to \square{}$ and for each term $t : A$ a
witness $\binlogrelTm{t} : \binlogrelTy{A}~\bareTm{t}~\monTm{t}$.

The logical relation employs a an inductively defined relation $\U_{\binlrel,i}$
between $\U_i^\disc := \bareTy{\square_i}$ and $\U_i^\mon := \monTy{\square_i}$
whose constructors are relational codes relating codes of discrete and monotone
These relational codes are then decoded to relations between the corresponding
decoded types thanks to ${ \El{} }_{\binlrel}$.
The main difficult case in establishing the logical relation lie in relating
the $\cas$s, since that's the main point of divergence of the two models.

\begin{lemma}[Basis lemma]\text{}
\begin{enumerate}
\item There exists a term $\cas_\binlrel : \binlogrelTy{\P (A\, B : \U).A \to B}~\bareTm{\cas}~\monTm{\cas}$.
\item More generally, if $\Gamma \caty t : A$ then $\binlogrelTy{\Gamma} \irty \binlogrelTm{t} : \binlogrelTy{A}~\bareTm{t}~\monTm{t}$.
\end{enumerate}
\end{lemma}
In particular \CCIC terms of ground types behave similarly in both models.

\begin{proof}

Expanding the type of $\cas_\binlrel$, we need to provide a
\[c_\binlrel = \cas_\binlrel\,A\,A'\,A_\binlrel\,B\,B'\,B_\binlrel\,a\,a'\,a_\binlrel
: \El_\binlrel\,B_\binlrel~(\bareTm{\cas}\,A\,B\,a)~(\monTm{\cas}\,A'\,B'\,a')\]
\begin{align*}
A &: \bareTy{\square{}_i},& A' &: \monTy{\square{}_i},& A_\binlrel &: \U_\binlrel\,A\,A',\\
B &: \bareTy{\square{}_i},& B' &: \monTy{\square{}_i},& B_\binlrel &: \U_\binlrel\,B\,B',\\
a &: \El\,A,& a' &: \El\,A',& a_\binlrel &: \El_\binlrel\,A_\binlrel~a~a'
\end{align*}
We proceed by induction on $A_\binlrel, B_\binlrel$, following the
defining cases for $\bareTm{\cas}$ (see \cref{fig:cast-implem-discrete}).

\noindent\textbf{Case $A_\binlrel =
\PiU_\binlrel\,A^\pidom_\binlrel\,A^\picod_\binlrel$ and
$B_\binlrel = \PiU_\binlrel\,B^\pidom_\binlrel\,B^\picod_\binlrel$:}
we pose ${A' = \PiU\,A'^\pidom\,A'^\picod}$ and ${B' = \PiU\,B'^\pidom\,B'^\picod}$
\newcommand{\ucast}[2]{\upcast^{#2}_{#1}}
\newcommand{\dcast}[2]{\downcast^{#1}_{#2}}
\begin{align*}
\monTm{\cas}~A'~B'~f' &= ~\dcast{\unkU}{B'}(\ucast{A'}{\unkU} f') \tag{by definition of $\monTm{\cas}$}\\
&= ~\dcast{\unkU \to \unkU}{B'}\circ \dcast{\unkU}{\unkU \to \unkU} \circ \ucast{\unkU \to \unkU}{\unkU} \circ \ucast{A'}{\unkU \to \unkU} (f)\tag{by decomposition of $\PiU \sqsubseteq \unkU$}\\
&= ~\dcast{\unkU \to \unkU}{B'}\circ \ucast{A'}{\unkU \to \unkU} (f) \tag{by section-retraction identity}\\
&= \l (b' : \El\,A'^\pidom).
~\letin{a'}{~\dcast{\unkU}{B'^\pidom}\circ\ucast{A'^\pidom}{\unkU} (b)}{}\tag{by def. of \eppair{} on $\Pi$}\\
&= \l (b' : \El\,A'^\pidom).
~\letin{a'}{\monTm{\cas}~B'^\pidom~A'^\pidom~b'}{} \tag{by definition of $\monTm{\cas}$}\\
\end{align*}

For any $b : \El\,B^\pidom$ and $b' : \El\,B'^\pidom$, $b_\binlrel :
\El_\binlrel\,B^\pidom_\binlrel\,b\,b'$, we have by inductive hypothesis
\[a_\binlrel := \binlogrelTm{\cas}\,B^\pidom_\binlrel\,A^\pidom_\binlrel\,b_\binlrel : \El_\binlrel~{A_\binlrel}~(\bareTm{\cas}\,B^\pidom\,A^\pidom\,b)~(\monTm{\cas}\,B'^\pidom\,A'^\pidom\,b')\]
so that, posing $a = \bareTm{\cas}\,B^\pidom\,A^\pidom\,b$ and $a' =
\monTm{\cas}\,B'^\pidom\,A'^\pidom\,b'$,
\[f_\binlrel\,a\,a'\,a_\binlrel : \El_\binlrel~(A^\picod_\binlrel\,a\,a'\,a_\binlrel)~(f\,a)~(f'\,a')\]
and by another application of the inductive hypothesis
\[\binlogrelTm{\cas}~(B^\picod_\binlrel\,b\,b'\,b_\binlrel)~(A^\picod_\binlrel\,a\,a'\,a_\binlrel)~(f_\binlrel\,a\,a'\,a_\binlrel)
\binlogrelTy{B^\picod_\binlrel\,b\,b'\,b_\binlrel}~(\bareTm{\cas}~A~B~f~a)~(\monTm{\cas}~A'~B'~f'~a')\]
Packing these together, we obtain a term
\[\binlogrelTm{\cas}~A_\binlrel~B_\binlrel~f_\binlrel
\El_\binlrel~(\PiU~B^\pidom_\binlrel~B^\picod_\binlrel)~(\bareTm{\cas}~A~B~f)~(\monTm{\cas}~A'~B'~f').\]

\noindent\textbf{Case $A_\binlrel =
\PiU_\binlrel\,A^\pidom_\binlrel\,A^\picod_\binlrel$ and
$B_\binlrel = \unkU[\binlrel]$:}
By definition of the logical relation at $\unkU[\binlrel]$, we need to build a
witness of type
\[\El_\binlrel~(\unkU^{\castOfPi{i}} \to \unkU^{\castOfPi{i}})~(\bareTm{\cas}~A~(\unkU \to\unkU)~f)~(\dcast{\unkU}{\unkU \to\unkU}(\monTm{\cas}~A'~\unkU~f'))\]
We compute that
\[\dcast{\unkU}{\unkU \to\unkU} (\monTm{\cas}\,A'\,\unkU\,f') =
~\dcast{\unkU}{\unkU \to\unkU} \circ \dcast{\unkU}{\unkU} \circ \ucast{A'}{\unkU}f' =
~\dcast{\unkU}{\unkU \to\unkU} \circ \ucast{A'}{\unkU}f' =
\monTm{\cas}\,A'\,(\unkU \to \unkU)\,f'
\]
So the result holds by induction hypothesis.

\noindent\textbf{Other cases with
$A_\binlrel = \PiU_\binlrel\,A^\pidom_\binlrel\,A^\picod_\binlrel$:}
It is enough to show that $\monTm{\cas}\,A'\,B'\,f' = \maltese_{B'}$ when $B' =
\maltese$ (trivial) or $\hd\,B' \neq \texttt{pi}$. The latter case holds because
$\dcast{\unkU}{\stalkCIC{}{c}} \ucast{\stalkCIC{}{c'}}{\unkU} x = \maltese_{\El_{\C}\,c}$ whenever $c
\neq c'$ and downcasts preserve $\maltese$.

\noindent\textbf{Case $A_\binlrel = \unkU[\binlrel]$,
$B_\binlrel = \PiU_\binlrel\,B^\pidom_\binlrel\,B^\picod_\binlrel$ and
$a = (\texttt{pi} ; f)$:}
By hypothesis, $a_\binlrel : \El_\binlrel~(\unkU \to
\unkU)~f~(\dcast{\unkU}{\unkU \to \unkU}a')$ and
$\monTm{\cas}~\unkU~B'~a' = \monTm{\cas}~(\unkU \to
\unkU)~B'~(\dcast{\unkU}{\unkU \to \unkU}a')$ so by induction hypothesis
\[\binlogrelTm{\cas}~(\unkU[\binlrel] \to_\binlrel
\unkU[\binlrel])~B_\binlrel~f~(\dcast{\unkU}{\unkU \to
\unkU}a')~a_\binlrel : \El_\binlrel\,B_\binlrel~(\bareTm{\cas}\,\unkU\,B\,(\texttt{pi};f))~(\monTm{\cas}\,\unkU\,B'\,a')\]

\noindent The others cases with $A_\binlrel = \unkU[\binlrel]$ proceed in a
similarly fashion.
All cases with $A_\binlrel = \maltese_\binlrel{}$ are immediate since
$\maltese^\disc$ and $\maltese^\mon$ are related at any related types.
Finally, the cases with $A_\binlrel{} = \natU_\binlrel$ follow the same pattern
as for $\PiU_\binlrel$.
\end{proof}

\section{Diverging terms denote as errors in $\omega$-cpos}
\label{sec:divergence-omega-cpo-model}

In this section we define a logical relation between \CCICP and \CICIRQ and
prove a fundamental lemma, obtaining~\cref{lem:diverge-err} as a corollary.
The logical relation is presented in
\cref{fig:logrel-ccicp-omega-cpo,fig:logrel-ccicp-omega-cpo-cont,fig:logrel-ccicp-omega-cpo-cont-cont}
and relates types $A$ in \CCICP with sub-$\omega$-cpos of $\unkMon$,
following the description of $\El$ in that model.
A type $A$ related to an $\omega$-cpo $A'$ by the logical relation, noted $A
\sim A'$, induces a relation between terms of type $A$ and elements of $A'$.
We use variables with $\varepsilon$ subscript to name proof witnesses of
relatedness between two objects, for instance $A_\varepsilon : A \sim A'$, and
bold variables such as $\GG, \DD$ for the corresponding double contexts
consisting of variable bindings $\divbind{a}{a'}{A_\varepsilon}$.
The projections $\tcol{\fs{\GG}}$ and $\sn{\GG}$ are then respectively contexts
in \CCICP and \CICIRQ.

The logical relation uses weak head reduction to characterize divergence.
We note $\tcol{t} \whred \tcol{u}$ when a \CCIC term $\tcol{t}$ reduces to a
weak head normal form, that is a term $\tcol{u}$ such that $\can\tcol{u}$ hold (see~\cref{fig:CCIC-canonical}), using
only weak head reduction steps.
We note $\tcol{t} \not\whred$ when weak head reduction paths from $\tcol{t}$ never reach a
weak head normal form, that is $\tcol{t}$ is unsolvable.

\begin{figure}[h]

\flushleft{}
\fbox{$\divrelCtx{\GG}$} logical relation between \CCICT contexts and

\begin{mathpar}
\inferrule{}{\divrelCtx{\cdot}}
\and
\inferrule
{ \divrelCtx{\GG}\\
A_\varepsilon : \divrelTy{\GG}{A}{A'}}
{ \divrelCtx{\GG, \divbind{a}{a'}{A_\varepsilon}}}
\and
\begin{array}{l@{~=~}l}
\fs\cdot& \tcol\cdot \\
\fs{(\GG , \divbind{a}{a'}{A_\varepsilon})} & \tcol{\fs\GG , a : A}
\end{array}
\end{mathpar}
\bigskip

\flushleft{}
\fbox{$\divrelTy{\GG}{A}{B}$} logical relation between \CCICP types $\tcol{A}$ and
$\omega$-cpos $B \subset \unkMon$.
\begin{mathpar}
\inferrule{\divrelTm{\GG}{T}{U}{\univDivrel}}
\end{mathpar}
\bigskip

\fbox{$\divrelTm{\GG}{t}{u}{\boolDivrel}$} logical relation between \CCICP terms
of type $\tcol{\bool}$ and elements of $\liftBool$.
\begin{mathpar}
\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\bool} \\
\tcol{t} \whred \tcol{\btrue} \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\btrue}{\boolDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\bool} \\
\tcol{t} \whred \tcol{\bfalse} \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\bfalse}{\boolDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\bool} \\
\tcol{t} \whred \tcol{\?_\bool} \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\lifttop{\liftBool}}{\boolDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\bool} \\
\tcol{t} \whred \tcol{\err_\bool} \vee \tcol{t} \not\whred \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\liftbot{\liftBool}}{\boolDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\bool} \\
\tcol{t}\whred \tcol{t'}\\
\divrelNe{\GG}{t'}{u}{\boolDivrel}
}{ \divrelTm{\GG}{t}{u}{\boolDivrel} }
\end{mathpar}
\bigskip

\fbox{$\divrelTm{\GG}{t}{u}{\natDivrel}$} logical relation between \CCICP terms
of type $\tcol{\nat}$ and elements of $\liftNat$.
\begin{mathpar}
\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\nat} \\
\tcol{t} \whred \tcol{0} \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{0}{\natDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\nat} \\
\tcol{t} \whred \tcol{\suc\,t'} \\
\divrelTm{\GG}{t'}{u'}{\natDivrel}
}{ \divrelTm{\GG}{t}{\suc\,u'}{\natDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\nat} \\
\tcol{t} \whred \tcol{\?_\nat} \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\lifttop{\liftNat}}{\natDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\nat} \\
\tcol{t} \whred \tcol{\err_\nat} \vee \tcol{t} \not\whred \\
\divrelCtx{\GG}
}{ \divrelTm{\GG}{t}{\liftbot{\liftNat}}{\natDivrel} }

\and

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\nat} \\
\tcol{t}\whred \tcol{t'}\\
\divrelNe{\GG}{t'}{u}{\natDivrel}
}{ \divrelTm{\GG}{t}{u}{\natDivrel} }
\end{mathpar}
\bigskip

\fbox{$\divrelTm{\GG}{t}{u}{\unkDivrel\,i}$} logical relation between \CCICP terms
of type $\tcol{\?_{\square_i}}$ and elements of $\unkMon[i]$.

\begin{mathpar}
\inferrule
{ \tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{\?_\square} \\
\tcol{t} \whred \tcol{\?_{\?_{\square_i}}}\\
\divrelCtx{\GG}}
\and
\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\?_\square} \\
\tcol{t} \whred \tcol{\err_{\?_{\square_i}}} \vee \tcol{t} \not\whred\\
\divrelCtx{\GG}}
\and
\inferrule
{ \tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{\?_\square} \quad
\tcol{t} \whred \tcol{\ascdom{t'}{A}{\?}} \quad
\divrelTm{\GG}{t'}{u'}{A_\varepsilon}}

\inferrule
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\?_\square} \quad
\tcol{t}\whred \tcol{t'}\quad
\divrelNe{\GG}{t'}{u}{\unkDivrel\,i}
}{ \divrelTm{\GG}{t}{u}{\unkDivrel\,i} }
\end{mathpar}
\caption{Logical relation between \CCICP and $\omega$-cpos}
\label{fig:logrel-ccicp-omega-cpo}
\end{figure}

\begin{figure}[h]
\flushleft
\fbox{$\divrelTm{\GG}{t}{u}{\errDivrel\,\tcol{A}}$} logical relation between \CCICP terms
of type $\tcol{A}$ and elements of $\unit$.

\begin{mathpar}
\inferrule
{\tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{A}}
\end{mathpar}
\bigskip

\fbox{$\divrelTm{\GG}{t}{u}{\univDivrel\,i}$} logical relation between \CCICP terms
of type $\tcol{\square_i}$ and elements of $\U_i$.

\begin{mathpar}
\inferrule[$\natDivrel$]
{ \tcol{\fs{\GG}}\vdash \tcol{T} \inferty \tcol{\square_i} \\
\tcol{T} \whred \tcol{\nat} \\
\divrelCtx{\GG} }
{ \divrelTm{\GG}{T}{\natU}{\univDivrel\,i}}
\and
\inferrule[$\unkDivrel$]{
\tcol{\fs{\GG}}\vdash \tcol{T} \inferty \tcol{\square_i} \\
\tcol{T} \whred \tcol{\?_{\square_i}} \\
\divrelCtx{\GG} }
{ \divrelTm{\GG}{T}{\unkU[i]}{\univDivrel\,i} }
\and

\inferrule[$\errDivrel$]{
\tcol{\fs{\GG}}\vdash \tcol{T} \inferty \tcol{\square_i} \\
\tcol{T} \whred \tcol{\err_{\square_i}} \vee \tcol{T} \not \whred \\
\divrelCtx{\GG}}
{\divrelTm{\GG}{T}{\errU}{\univDivrel\,i} }

\and

\inferrule[$\univDivrel$]{
\tcol{\fs{\GG}}\vdash \tcol{T} \inferty \tcol{\square_i} \\
\tcol{T} \whred \tcol{\square_j} \\
\divrelCtx{\GG} }

\and

\inferrule[$\piDivrel$]
\tcol{\fs{\GG}}\vdash \tcol{T} \inferty \tcol{\square_i} \\
\tcol{T} \whred \tcol{\P(a : A)\,B}\\
A_\varepsilon : \forall \rho : \DD \subseteq \GG, \divrelTm{\DD}{A[\fs\rho]}{A'[\sn\rho]}{\univDivrel\,i} \\
\forall \rho : \DD \subseteq \GG,
\divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho} \implies \divrelTm{\GG}{B[a]}{B'[a']}{\univDivrel\,i}}
{\divrelTm{\GG}{T}{\PiU\,A'\,(\lambda(a' : A').B')}{\univDivrel\,i}}

\and

\inferrule[$\neDivrel$]
{ \tcol{\fs{\GG{}}} \vdash \tcol{t} \inferty \tcol{\square_i} \\
\tcol{t}\whred \tcol{t'}\\
\divrelNe{\GG}{t'}{u}{\univDivrel\,i}
}{ \divrelTm{\GG}{t}{u}{\univDivrel\,i} }

\end{mathpar}
\bigskip

\fbox{$\divrelTm{\GG}{t}{u}{\piDivrel\,A_\varepsilon\,B_\varepsilon}$} logical relation between \CCICP terms
of  $\Pi$ type.
\begin{mathpar}
\inferrule
{\forall (\rho : \DD \subseteq \GG)~(a_\varepsilon : \divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho}),
\end{mathpar}

\begin{itemize}
\item $\tcol{\fs{\GG}} \vdash \tcol{t} \inferty \tcol{\Pi\,(a : A)\,B}$,
\item $\sn{\GG} \irty u : \Picont\,(a' : A')\,B'$,
\item $A_\varepsilon : \forall \rho : \DD \subseteq \GG, \divrelTm{\DD}{A[\fs{\rho}]}{A'[\sn{\rho}]}{\univDivrel\,i}$
\item $B_\varepsilon : \forall \rho : \DD \subseteq \GG, \divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho} \implies \divrelTm{\DD}{B[a]}{B'[a']}{\univDivrel\,i}$
\end{itemize}
\caption{Logical relation between \CCICP and $\omega$-cpos}
\label{fig:logrel-ccicp-omega-cpo-cont}
\end{figure}

\begin{figure}[h]
\flushleft

\fbox{$\divrelTm{\GG}{t}{u}{\neDivrel\,A_\varepsilon}$} logical relation on \CCICP terms
of a neutral type $\tcol{A}$ ($A_\varepsilon : \divrelTy{\GG}{A}{A'}$).

\begin{mathpar}
\inferrule
\end{mathpar}
\bigskip

\fbox{$\divrelNe{\GG}{t}{u}{A_\varepsilon}$} logical relation on neutral
\CCICP terms (excerpt).

\begin{mathpar}
\inferrule{
\divrelCtx{\GG} \\
\divbind{a}{a'}{A_\varepsilon} \in \GG }

\and

\inferrule{
\divrelNe{\GG}{f}{f'}{\piDivrel\,A_\varepsilon\,B_\varepsilon}\\
t_\varepsilon : \divrelTm{\GG}{t}{t'}{A_\varepsilon}}

\and

\inferrule{
b_\varepsilon : \divrelNe{\GG}{b}{b'}{\boolDivrel}\\
P_\varepsilon : \divrelTy{\GG,\divbind{z}{z'}{\boolDivrel}}{P}{P'} \\
\divrelTm{\GG}{t_\btrue}{t'_\btrue}{P_\varepsilon[\tcol{\btrue} \sim \btrue]}\\
\divrelTm{\GG}{t_\bfalse}{t'_\bfalse}{P_\varepsilon[\tcol{\bfalse} \sim \bfalse]}
}{\divrelNe{\GG}{\match{\bool}{b}{z.P}{(t_{\btrue}, t_{\bfalse})}}{\match{\bool}{b'}{z'.P'}{(t'_{\btrue}, t'_{\bfalse})}}{P_\varepsilon[b_\varepsilon]}}

\and

\inferrule{
A_\varepsilon : \divrelNe{\GG}{A}{A'}{\univDivrel}\\

\and

\inferrule{
A_\varepsilon : \divrelNe{\GG}{A}{A'}{\univDivrel}\\

\and

\inferrule
A_\varepsilon : \divrelNe{\GG}{A}{A'}{\univDivrel}\\
B_\varepsilon : \divrelTm{\GG}{B}{B'}{\univDivrel} \\
\divrelTm{\GG}{t}{t'}{A_\varepsilon}
\end{mathpar}

\caption{Logical relation between \CCICP and $\omega$-cpos}
\label{fig:logrel-ccicp-omega-cpo-cont-cont}
\end{figure}

We first state a lemma making explicit how divergence is accounted for by the
logical relation.

\begin{lemma}[Diverging terms relate to errors]
\label{lem:div-to-error}\text{}
\begin{enumerate}
\item If $\tcol{\fs\GG} \vdash \tcol{t} : \tcol{T}$, $T_\varepsilon :
\divrelTy{\GG}{T}{T'}$ and $\tcol{t}
\not\whred$ then $\divrelTm{\GG}{t}{\err_{T'}}{T_\varepsilon}$.
\item Conversely, if $\tcol{\Gamma} \vdash \tcol{t} : \tcol{T}$, $T_\varepsilon :
\divrelTy{\GG}{T}{T'}$, $\divrelTm{\GG}{t}{t'}{T_\varepsilon}$ and $\tcol{t}
\not\whred$ then $t' = \err_{T'}$.
\end{enumerate}
\end{lemma}
\begin{proof}
In the two parts of the lemma, we proceed by induction on $T_\varepsilon$.
For the first part, the cases $T_\varepsilon = \univDivrel, \natDivrel, \boolDivrel$ and
$\unkDivrel$ are immediate because in each case a rule apply for diverging terms.
If $T_\varepsilon = \errDivrel$, then
$\divrelTm{\GG}{t}{\unitK}{T_\varepsilon}$ which is enough because $\unitK =
\err_{\unit} = \err_{\El\,\errU} = \err_{\El\,T'}$.
Finally, if $T_\varepsilon = \piDivrel\,A_\varepsilon\,B_\varepsilon$, then
for any $\rho : \DD \subset \GG$ and $a_\varepsilon :
\divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho}$
we have that $\tcol{\fs\GG} \vdash \tcol{t[\fs{\rho}]~a} : \tcol{B[\fs{\rho},a]}$,
$B_\varepsilon\,\rho\,a_\varepsilon :
\divrelTy{\DD}{B[\fs{\rho},a]}{B'[\sn{\rho}, a']}$ and
$\tcol{t~a} \not\whred$, so by induction hypothesis
hence $\divrelTm{\GG}{t}{\err_{\PiU\,A'\,B'}}{T_\varepsilon}$.

We now turn to the second part of the lemma.
When $T_\varepsilon = \univDivrel, \natDivrel, \boolDivrel, \unkDivrel$ and
$\errDivrel$, there is exactly one rule that apply to relate to a term without
weak head normal form $\tcol{t}$ so that necessarily $t' = \err_{T'}$.
When $T_\varepsilon = \piDivrel\,A_\varepsilon\,B_\varepsilon$,  any $\rho
: \DD \subset \GG$ and $a_\varepsilon:
\divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho}$ we have that
$B_\varepsilon\,\rho\,a_\varepsilon : \divrelTy{\DD}{B[\fs{\rho},a]}{B'[\sn{\rho}, a']}$,
$\divrelTm{\DD}{t[\fs{\rho}]~a}{t'[\sn{\rho}]~a'}{B_\varepsilon\,\rho\,a_\varepsilon}$ and
$\tcol{t~a} \not\whred$, so by induction hypothesis $t'\,a' =
\err_{B'[\sn{\rho}, a']}$.
Taking $\rho$ to be the weakening $\GG, \divbind{a}{a'}{A_\varepsilon} \subset
\GG$, we have by function extensionality that $t' = \lambda(a':A'). \err_{B'}
= \err_{\PiU\,A'\,B'}$.
\end{proof}

\begin{lemma}[Fundamental lemma]\text{}
\begin{itemize}
\item If $\tcol{\Gamma} \vdash$ then there exists $\GG$ such that
$\divrelCtx{\GG}$, $\tcol{\fs\GG} = \tcol{\Gamma}$ and $\sn{\GG} =
\monTy{\tcol{\Gamma}}$ ;
\item If $\tcol{\Gamma} \vdash \tcol{T} \inferty \tcol{\square_i}$ there
exists a derivation $T_\varepsilon : \divrelTy{\GG}{T}{\monTy{\tcol{T}}}$
\item  If $\tcol{\Gamma} \vdash \tcol{t} \inferty \tcol{T}$ then there exists
a derivation $ t_\varepsilon : \divrelTm{\GG}{t}{\monTm{\tcol{t}}}{T_\varepsilon}$
\item If $\tcol{\Gamma} \vdash \tcol{T} \inferty \tcol{\square_i}$,
$\tcol{\Gamma} \vdash \tcol{T'} \inferty \tcol{\square_i}$ and  $\tcol{T} \conv \tcol{T'}$ then $\monTy{\tcol{T}} =
\monTy{\tcol{T}'}$ and $T_\varepsilon = T'_\varepsilon : \divrelTy{\GG}{T}{\monTy{\tcol{T}}}$.
\end{itemize}
\end{lemma}

\begin{proof}
Since the translation $\monTy{-}$ underly a model of \CCICT, it sends
convertible types $\tcol{T}, \tcol{T'}$ in the source to provably equal types
in the target  $\monTy{\tcol{T}} = \monTy{\tcol{T}'}$, proving the last claim.

The three other claims are proved by mutual induction on the input derivation,
assuming an undirected variant of the rules
in~\cref{fig:ccic-typing,fig:bidir}, which is possible
Concretely, this modification means that we assume additional well-formedness
premises in the derivations, \eg for contexts and types, and do not show that
input well-formedness is preserved.
Moreover the induction hypothesis needs to be strenghened to quantify over an
arbitrary context $\DD$ with a substition $\sigma : \DD \to \GG$ whose
components are related according to the logical relation.

For contexts, if the derivation ends with a rule \nameref{infrule:cic-axiom}, it is enough take $\GG = \cdot$.
If it ends with \nameref{infrule:cic-concat}, then by induction hypothesis
there exists $\GG$ and $A_\varepsilon$ such that $\tcol{\fs{\GG}} =
\tcol{\Gamma}$, $\sn{\GG} = \monTy{\tcol{\Gamma}}$, $\divrelCtx{\GG}$ and
$A_\varepsilon : \divrelTy{\GG}{A}{\monTy{\tcol{A}}}$, so taking $\GG,
\divbind{a}{a'}{A_\varepsilon}$ suffices.

For \nameref{infrule:cic-univ} by induction hypothesis $\divrelCtx{\GG}$ with
$\tcol{\fs{\GG}} = \tcol\Gamma$. Moreover, $\tcol\Gamma \vdash
\tcol{\square_i} \inferty \tcol{\square_{i+1}}$ and $\monTm{\tcol{\square_i}}
= \uU_i$ so
$\divrelTm{\GG}{\square_i}{\monTm{\tcol{\square_i}}}{\univDivrel\,(i+1)}$ and
The rules \nameref{infrule:cic-ind} (for $\nat, \bool$) and
\nameref{infrule:cic-cons} (for $\natzero, \suc, \btrue, \bfalse$),
introducing types and terms that are already
in weak head normal form follow the same pattern as \nameref{infrule:cic-univ}.
In the case of the rules \nameref{infrule:ccic-prod} and
\nameref{infrule:cic-abs}, the context needs to be extended and we need to
take advantage of the full induction hypothesis strenghened under arbitrary
reducible substitutions.

Dually, the rule \nameref{infrule:cic-app} is immediate by induction
hypothesis and the definition the logical relation at function types.
A bit more work is needed for the rule \nameref{infrule:cic-fix} for
$\ind_\bool$ and $\ind_\nat$, doing a case analysis on the proof of
relatedness of their main argument.
If the main argument diverges, then the applied eliminator diverges too so it
is related to $\err$ which is its translation because eliminators send errors
at an inductive type to errors at the adequate type in $\omega$-cpos.
Otherwise the main argument weak head reduces to a normal form and we can
conclude by induction hypothesis and closure by anti-reduction.

For the variable case, rule \nameref{infrule:cic-var}, we can show by
induction on the proof of relatedness of its type that it is related to its
$\eta$-expansion at $\Pi$ types an to itself at any other type using the rules
for neutrals.
We conclude by extensionality of the $\omega$-cpo model.

Conversion rules \nameref{infrule:cic-check},
\nameref{infrule:cic-prod-inf}, \nameref{infrule:cic-ind-inf} and
\nameref{infrule:cic-univ-inf} satisfy the fundamental lemma because
convertible types induce the same relation on their term.

For \nameref{infrule:ccic-err}, we have by induction hypothesis that
$T_\varepsilon : \divrelTm{\GG}{T}{\monTm{\tcol{T}}}{\univDivrel}$.
By case analysis, $T_\varepsilon$ is necessarily one of $\errDivrel,\piDivrel, \unkDivrel, \boolDivrel,
\natDivrel$ or $ \univDivrel$.
If $T_\varepsilon = \errDivrel\,\tcol{T}$ then
$\divrelTm{\GG}{\err_T}{\unitK}{\errDivrel\,\tcol{T}}$ since $\tcol{\fs\GG} \vdash
\tcol{\err_T} \inferty{T}$, and we can conclude using extensionality of $\unit
= \monTy{\tcol{T}}$, that is $\monTm{\tcol{\err_T}} = \unitK$.
If $T_\varepsilon = \piDivrel\,A_\varepsilon\,B_\varepsilon$, then for any
$\rho : \DD \subset \GG$ and $a_\varepsilon :
\divrelTm{\DD}{a}{a'}{A_\varepsilon\,\rho}$ we have that
$\tcol{T[\fs\rho]} \whred \tcol{\Pi(a:A)B}$ and $\tcol{\err_{T}~a} \whred
\tcol{\err_{B[a]}}$, so we conclude this case by induction hypothesis
closure by anti-reduction and the fact that $\monTm{\tcol{\err_{B[a]}}} =
\err_{\monTm{B[a]}} = \err_{\monTm{B}[a']}$.

In all the other cases $\tcol{T}$ weak head reduces to a type in weak head
normal form $\tcol{\?_\square}, \tcol{\square_i}, \tcol{\nat}$ or
$\tcol{\bool}$, and a corresponding rule is present in the logical relation to
conclude directly.
A similar proof apply for the rule \nameref{infrule:ccic-unk}.

Finally, for the rule \nameref{infrule:ccic-cast} with conclusion
$\tcol{\Gamma} \vdash \tcol{\ascdom{t}{A}{B}} \inferty \tcol{B}$, we have by
induction hypothesis we have that $\divrelCtx{\GG}, {A_\varepsilon :
\divrelTy{\GG}{A}{\monTy{\tcol{A}}}}, B_\varepsilon :
\divrelTy{\GG}{B}{\monTy{\tcol{B}}}$ and
By analysing all possible weak head reduction paths from
$\tcol{\ascdom{t}{A}{B}}$, either:
\begin{description}
\item[(a)] $\tcol{\ascdom{t}{A}{B}} \whred \tcol{u}$
such that $\divrelTm{\GG}{u}{\monTm{\tcol{u}}}{B_\varepsilon}$ using
inversions on $A_\varepsilon, B_\varepsilon$ and $t_\varepsilon$, or
\item[(b)] one of
$\tcol{A}$, $\tcol{B}$ or $\tcol{t}$ never reduces to a weak head normal form.
\end{description}
In case \textbf{(a)}, we conclude that
by closure under anti-reduction and using the fact that
$\monTm{\tcol{\ascdom{t}{A}{B}}} = \monTm{\tcol{u}}$ (because $\monTm{-}$ maps
convertible terms to equal terms in the model).
In case \textbf{(b)}, we have that
$\divrelTm{\GG}{\ascdom{t}{A}{B}}{\err_{\monTm{\tcol{B}}}}{B_\varepsilon}$ by
the first part of~\cref{lem:div-to-error} and the second part of that lemma
ensures that one of $\monTm{\tcol{A}}$, $\monTm{\tcol{B}}$ or
$\monTm{\tcol{t}}$ is an error at the adequate type so that
$\monTm{\tcol{\ascdom{t}{A}{B}}} =
\downcast^{\unkU}_{\monTm{\tcol{B}}}\upcast^{\unkU}_{\monTm{\tcol{A}}}\monTm{\tcol{t}}
= \err_{\monTm{\tcol{B}}}$.
\end{proof}

\begin{corollary}
If $\tcol{\Gamma} \vdash \tcol{t} \inferty \tcol{T}$ and $\tcol{t} \not\whred$
then $\monTm{\tcol{t}} = \err_{\monTm{\tcol{T}}}$.
\end{corollary}
\begin{proof}
By the fundamental lemma, $\divrelTm{\GG}{t}{\monTm{\tcol{t}}}{T_\varepsilon}$
with $T_\varepsilon : \divrelTm{\GG}{T}{\monTm{\tcol{T}}}{\univDivrel}$
and by the second part of \cref{lem:div-to-error}, $\monTm{\tcol{t}}
= \err_{\monTm{\tcol{T}}}$.
\end{proof}

\section{A Direct Presentation of Vectors}
\label{sec:case-vectors-appendix}

\begin{figure}
\small
\begin{mathpar}
\inferrule{ }{\can{\Gnil}{A}} \and
\inferrule{ }{\can{(\Gcons{A}{a}{n}{v})}} \and
\inferrule{  }{\can{\GnilU{A}}}
\and
\inferrule{ }{\can{(\GconsU{A}{a}{n}{v})}}
\\
\inferrule{\neu{v} \quad \vee \quad \neu{n} \quad \vee \quad \neu{m} }{\neu{(\ascdom{v}{\Gvect{A}{n}}{\Gvect{B}{m}}})}
\and
\inferrule{\neu{v}}{\neu{(\GvectRec}{P}{P_{nil}}{P_{cons}}{v})}
\\
% \\
\inferrule{\Gamma \vdash A \checkty \square{}_{i}}{\Gamma \vdash \GnilULevel{A}{i} \inferty
\Gvect{A}{\?_\nat}}[nilu]
\and
\inferrule{\Gamma \vdash A \checkty \square{}_{i} \\ \Gamma \vdash
a \checkty A \\ \Gamma \vdash
n \checkty \nat \\ \Gamma \vdash v \checkty \Gvect{A}{n}
}{\Gamma \vdash \GconsULevel{A}{a}{n}{v}{i} \inferty
\Gvect{A}{\?_\nat}}[consu]
\\
\\
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{\Gnil{A}}
\and
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{(\Gcons{A}{a}{n}{v})}
P_{cons}~a~n~(\GvectRec{P}{P_{nil}}{P_{cons}}{v}) \hfill
\and
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{\err_{\Gvect{A}{n}}}
\err_{P~{\err_{\Gvect{A}{n}}}}\hfill
\and
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{\?_{\Gvect{A}{n}}}
\?_{P~{\?_{\Gvect{A}{n}}}}\hfill
\\
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{\GnilU{A}}
{\ascdom{(\GvectRec{P}{P_{nil}}{P_{cons}}{\Gnil{A}})}{P~0}{P~\?_\nat} \hfill
\\
\redrule{
\GvectRec{P}{P_{nil}}{P_{cons}}{(\GconsU{A}{a}{n}{v})}
\\
\myflushright \ascdom{(\GvectRec{P}{P_{nil}}{P_{cons}}{(\Gcons{A}{a}{n}{v})})}{P~(S~n)}{P~\?_\nat}
\\
\redrule{
\ascdom{\Gnil{A}}{\Gvect{A}{0}}{\Gvect{B}{0}}
\Gnil{B} \hfill
\and
\redrule{
\ascdom{\Gnil{A}}{\Gvect{A}{0}}{\Gvect{B}{(S~n)}}
\err_{\Gvect{B}{(S~n)}}\hfill
\and
\redrule{
\ascdom{\Gnil{A}}{\Gvect{A}{0}}{\Gvect{B}{\?_\nat}}
\GnilU{B}
\hfill
\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{(S~m)}}
\hfill}[V-cons]\label{red:v-S}
\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{0}}
\err_{\Gvect{B}{0}} \myflushright
\\
\redrule{
\ascdom{(\Gcons{A}{a}{k}{v})}{\Gvect{A}{(S~n)}}{\Gvect{B}{\?_\nat}}
\GconsU{B}{(\ascdom{a}{A}{B})}{n}{(\ascdom{v}{\Gvect{A}{k}}{\Gvect{B}{n}})}
\hfill
\\
\redrule{
\ascdom{\GnilU{A}}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{\?_\nat}}
{ \GnilU{B} \hfill
\\
\redrule{
\ascdom{\GnilU{A}}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{0}}
{ \Gnil{B} \hfill
\\
\redrule{
\ascdom{\GnilU{A}}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{(S~n)}}
{ \err_{\Gvect{B}{(S~n)}} \hfill
\\
\redrule{
\ascdom{(\GconsU{A}{a}{k}{v})}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{\?_{\nat}}}
\GconsU{B}{(\ascdom{a}{A}{B})}{k}{(\ascdom{v}{\Gvect{A}{k}}{\Gvect{B}{k}})} \hfill
\\
\redrule{
\ascdom{(\GconsU{A}{a}{k}{v})}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{0}}
\err_{\Gvect{B}{0}}  \hfill
\\
\redrule{
\ascdom{(\GconsU{A}{a}{k}{v})}{\Gvect{A}{\?_{\nat}}}{\Gvect{B}{(S~n)}}
{ \myflushright
\\
\myflushright
\Gcons{B}{(\ascdom{a}{A}{B})}{n}{(\ascdom{v}{\Gvect{A}{k}}{\Gvect{B}{n}})}
\\
\redrule{
\ascdom{\?_{\Gvect{A}{n}}}{\Gvect{A}{n}}{\Gvect{B}{m}}
\?_{\Gvect{B}{m}}\myflushright m,n \in \{ 0, S~m,
\?_\nat , \err_\nat \}
\and
\redrule{
\ascdom{\err_{\Gvect{A}{n}}}{\Gvect{A}{n}}{\Gvect{B}{m}}
\err_{\Gvect{B}{m}}\myflushright m,n \in \{ 0, S~m,
\?_\nat , \err_\nat \}
\and
\redrule{
\ascdom{v}{\Gvect{A}{n}}{\Gvect{B}{\err_\nat}}
\err_{\Gvect{B}{\err_\nat}}\myflushright n \in \{ 0, S~m,
\?_\nat , \err_\nat \} \mbox{ and } v \neq \?_{\Gvect{A}{n}}

\end{mathpar}
\label{fig:vectors}
\caption{Canonical forms and reduction rule for vectors.}
\end{figure}

Vectors have two new normal forms, corresponding to cast of
\coqe{nil} and \coqe{cons} to $\Gvect{A}{\?_{\nat}}$. The difference
with the treatment of the universe is that the corresponding term,
for instance $\ascdom{t}{\Gvect{A}{n}}{\Gvect{A}{\?_{\nat}}}$ for the
case of \coqe{nil}, can not be considered as canonical form because
they involve a non-linear occurrence of $A$.
To remedy to this issue, we add two new canonical forms ($\GnilU{A}$ and
$\GconsU{A}{a}{n}{v}$) to vectors
with introduction typing rules defined in \cref{fig:vectors}.

Regarding cast on vectors, it does not only compute in the argument of
the cast as it is the case for inductive types without indices, but it
also computes on the indices.
That is, a cast on vectors is neutral when either one of the indices
is neutral or the argument is neutral (see~\cref{fig:vectors}).
Other kind of neutral can be derived from the one of inductive types
without indices and are omitted here.

Similarly, we do not detail the other typing rules for vectors as they
are similar to the one for inductive types wihtout indices, and focus
on explaining the new reduction rules, presented also in
\cref{fig:vectors}.

The two first reduction rules \nameref{red:v-rect-nil} and
\nameref{red:v-rect-cons} are standard reduction rules in \CIC for the
recursor \texttt{vect\_rect} on vectors.
The rules \nameref{red:v-rect-err}  and \nameref{red:v-rect-unk} are
the standard rules dealing with exceptions.
Additionally, there are two computation rules for the eliminator on
the two new constructors \nameref{red:v-rect-unk-0} and
\nameref{red:v-rect-unk-S} which basically consist in the underlying
non-exceptional constructor to the eliminator and cast the result back
to $P~\?_\nat$.
This rule somehow transfers the cast on vectors to a cast on
the returned type of the predicate.

Finally, there are rules to conduct casts between vectors
in canonical forms.
The last three rules (\nameref{red:v-unk}, \nameref{red:v-err} and
\nameref{red:v-to-err}) are simply propogation of errors.
Then, there remains 12 rules, 3 by constructors of vectors. We just
explain the one on \coqe{cons}.
Rule~\nameref{red:v-S} applies when both indices of the form $S$
of somthing and progates the cast of the arguments, as does the
standard rule for casting a constructor.
Rule~\nameref{red:v-S0} detects that the indices do not match and
raise an error.
Finally, Rule~\nameref{red:v-S?} propagates the cast on the arguments,
but this time applied to $\GconsUName$, thus converting precise
information to a less precise information.

\ifleftovers

\section{Leftovers}

\subsection{Optimized Cast}

The last definition corresponds to a usual optimization of elaboration to a cast
calculus: why insert a run-time check when you know at typing time already that
the check will always succeed? Thus, a $\cas$ operator should only be inserted
by elaboration when the types are not the same (\ie convertible). Although with
closed types this is merely for performance purposes, it becomes crucial for us,
as types can contain variables that block reduction of the $\cas$ operator:
$\cast{A}{A}{t}$ does not reduce, because $\cas$ waits for the head constructor
of $A$ to appear. Even though one could prove that $\cast{A}{A}{t} = t$ in the
models we consider, the fact that this equality is not definitional is enough to
threaten theoretical properties, such as conservativity, because it blocks reduction.

\begin{definition}[Optimized cast]
Define the optimized cast $\ocast{A}{B}{t}$ to be $t$ if $A \conv B$, and $\cast{A}{B}{t}$ otherwise.
\end{definition}

Note that this cast can only be defined in a setting where conversion is decidable. If both $A$ and $B$ are well-typed, this depends on the normalization properties of the system: if the system normalizes, conversion is decidable (using normal forms), but if it does not then it is not. Thus, when considering the non-normalizing variants of \CCIC, we restrict this optimized cast to the \CIC fragment, that still normalizes. In other words, a cast is always inserted between gradual types, even if it is not needed.

It is really an optimization, in the following sense.
\begin{proposition}[Correction of the optimized cast]
If $\Gamma \vdash A : \square{}$ and $\Gamma \vdash B : \square{}$ one has $\Gamma \vdash \ocast{A}{B}{t} : B$ if and only if $\Gamma \vdash \cast{A}{B}{t} : B$.
\end{proposition}

\begin{lemma}[Syntactic precision respects optimized cast]
If $\Gamma.1 \vdash t : A$, $\Gamma.1 \vdash B : \square$, $\Gamma.2 \vdash t' : A'$, $\Gamma.2 \vdash B' : \square$ and we have the precision relations $\Gamma \vdash A \capre A'$, $\Gamma \vdash B \capre B'$ and $\Gamma \vdash t \capre t'$, then $\ocast{A'}{B'}{t'} \rtred s'$ for some $s'$ such that $\Gamma \vdash s \capre s'$.
\end{lemma}

\begin{proof}
If both casts optimize or do not optimize, no reduction is needed and the pointwise precision suffice. If the cast on the left is not optimized, and the one on the right is, we use the corresponding non-diagonal rule for the cast, and also no reduction is needed. The hard case is when the cast on the left is optimized, but not the one on the right. Then we can take $T$ to be the normal form of both $A$ and $B$, and we have $\Gamma \vdash t : T$. We can simulate this reduction, and thus get $A' \rtred A''$ and $B' \rtred B''$ for some $A''$ and $B''$ such that $\Gamma \vdash T \capre A''$ and $\Gamma \vdash T \capre B''$. Thus, $\cast{A'}{B'}{t'} \rtred \cast{A''}{B''}{t'}$, and now we can conclude with the non-diagonal rule for the cast.
\end{proof}

\fi

\fi

\end{document}