distinct type variables such that $X \notin \fv(B)$.  Then
$\subst{\subst{e}{X}{A}}{Y}{B} \alEq
\subst{\subst{e}{Y}{B}}{X}{\subst{A}{Y}{B}}$
\end{lemma}
\begin{proof}
By induction on the structure of $e$.
\end{proof}

\begin{proof}[Proof of \Lem{decl_subst}]
The two parts are proven separately, each by induction on the
derivation of the second premise ($\judgD{\Gamma, x \tas A, \Delta}$
for the first part, $\judgD{\Gamma, X \kas K, \Delta}$ for the
For the context formation judgment, the proofs proceed by a local
induction on the structure of $\Delta$.
We show the cases for \ruleref{K-Var} and
\rulerefN{ST-Beta1}{ST-$\beta_1$} for the second part of the lemma.
The other cases are similar.
\begin{itemize}
\item \emph{Case \ruleref{K-Var}.}
$\; \genjudg$ is $X \kin J$ and we have
$\ctxD{\Gamma, X \kas K, \Delta}$ and
$(\Gamma, X \kas K, \Delta)(Y) = J$.
By the IH, we get $\ctxD{\Gamma, \subst{\Delta}{X}{A}}$.
We distinguish two sub-cases based on whether $Y = X$.
\begin{itemize}
\item \emph{Sub-case $Y = X$.}
We want to show that
$\Gamma, \subst{\Delta}{X}{A} \ts A \kin \subst{K}{X}{A}$.
By well-scopedness, $X$ does not occur freely in $K$, so we have
$\subst{K}{X}{A} \alEq K$.
The desired result follows from applying iterated
weakening~(\Cor{decl_iter_weaken}) to the premise
$\Gamma \ts A \kin K$.
\item \emph{Sub-case $Y \neq X$.}
We want to show that
$\Gamma, \subst{\Delta}{X}{A} \ts Y \kin \subst{J}{X}{A}$.
Since the domains of $\Gamma$ and $\Delta$ are disjoint, $Y$
must appear either in $\Gamma$ or $\Delta$ but not in both.
If $Y \in \dom(\Gamma)$, then $X$ does not occur freely in
$J = \Gamma(Y)$ and hence
$(\Gamma, \subst{\Delta}{X}{A})(Y) = J \alEq \subst{J}{X}{A}$.
$(\Gamma, \subst{\Delta}{X}{A})(Y) = (\subst{\Delta}{X}{A})(Y) =
\subst{J}{X}{A}$.
In either case we conclude by~\ruleref{K-Var}.
\end{itemize}

\item \emph{Case \rulerefN{ST-Beta1}{ST-$\beta_1$}.}
$\; \genjudg$ is
$\app{(\lam{Y}{J_1}{B_1})}{B_2} \tsub \subst{B_1}{X}{B_2} \kin
\subst{J_2}{X}{B_2}$ and we have
$\Gamma, X \kas K, \Delta, Y \kas J_1 \ts B_1 \kin J_2$ and
$\Gamma, X \kas K, \Delta \ts B_2 \kin J_1$.
By the IH we get
\begin{alignat*}{3}
\Gamma, \subst{\Delta}{X}{A}&, Y \kas \subst{J_1}{X}{A} &\;&\ts \;
\subst{B_1}{X}{A} \; \kin \; \subst{J_2}{X}{A} &&\text{ and}\\
\Gamma, \subst{\Delta}{X}{A}& &\;&\ts \; \subst{B_2}{X}{A} \;
\kin \; \subst{J_1}{X}{A}.
\end{alignat*}

Applying \rulerefN{ST-Beta1}{ST-$\beta_1$}, we obtain
\begin{align*}
\Gamma, \subst{\Delta}{X}{A} \quad \ts \quad
\subst{(\app{(\lam{Y}{J_1}{B_1})}{B_2})}{X}{A} \quad \tsub &\quad
\subst{\subst{B_1}{X}{A}}{Y}{\subst{B_2}{X}{A}} \\
\kin \,{} &\quad \subst{\subst{K}{X}{A}}{Y}{\subst{B_2}{X}{A}}
\end{align*}
and using \Lem{sub_commutes} twice, it follows that
\[\Gamma, \subst{\Delta}{X}{A} \ts
\subst{(\app{(\lam{Y}{J_1}{B_1})}{B_2})}{X}{A} \tsub
\subst{\subst{B_1}{Y}{B_2}}{X}{A}
\kin  \subst{\subst{K}{Y}{B_2}}{X}{A}\]
which concludes the case.\qedhere
\end{itemize}
\end{proof}

\subsection{Admissible Order-Theoretic Rules}
\label{sec:decl_order}

The rules~\ruleref{ST-Refl} and \ruleref{ST-Trans} establish that
subtyping is a preorder.
Via~\ruleref{ST-AntiSym}, we can lift these
properties to type equality, and show that the latter is symmetric.
Together, these properties make type equality an equivalence relation.
\begin{corollary} Type equality is an equivalence, \ie the following
equality rules are admissible.
\end{corollary}
\begin{center}
\infruleSimp[TEq-Refl]
{\Gamma \ts A \kin K}
{\Gamma \ts A \teq A \kin K}
\hspace{4em}
\infruleSimp[TEq-Sym]
{\Gamma \ts A \teq B \kin K}
{\Gamma \ts B \teq A \kin K}
\medskip

\infruleSimp[TEq-Trans]
{\Gamma \ts A \teq B \kin K  \andalso  B \teq C \kin K}
{\Gamma \ts A \teq C \kin K}
\medskip
\end{center}
The same is true of kind equality, though we first have to establish
that subkinding is a preorder.
\begin{lemma} Subkinding is a preorder, \ie the following
subkinding rules are admissible.
\end{lemma}
\begin{center}
\infruleSimp[KS-Refl]
{\Gamma \ts K \tsub K}
\hspace{3em}
\infruleSimp[KS-Trans]
{\Gamma \ts K \tsub J  \andalso  J \tsub L}
{\Gamma \ts K \tsub L}
\end{center}
\begin{proof}
Separately for each rule, by structural induction on $K$ for
\ruleref{KS-Refl} and on $J$ for \ruleref{KS-Trans}.  For the type
interval cases we use the corresponding order-theoretic properties
of subtyping.  The proof of transitivity uses context narrowing
(\Lem{decl_weak_narrow}) and context validity (\Lem{decl_ctx_valid})
for subkinding in the case where $J = \dfun{X}{J_1}{J_2}$.
\end{proof}

\begin{corollary} Kind equality is an equivalence, \ie the following
equality rules are admissible.
\end{corollary}
\begin{center}
\infruleSimp[KEq-Refl]
{\Gamma \ts K \teq K}
\hspace{2em}
\infruleSimp[KEq-Trans]
{\Gamma \ts K \teq J  \andalso  J \teq L}
{\Gamma \ts K \teq L}
\hspace{2em}
\infruleSimp[KEq-Sym]
{\Gamma \ts K \teq J}
{\Gamma \ts J \teq K}
\medskip
\end{center}
In addition, the following variants of subtyping and subkinding
reflexivity are also admissible, which makes the subtyping and
subkinding relations partial orders \wrt type and kind equality.
\begin{center}
\medskip
\infruleSimp[ST-Refl-TEq]
{\Gamma \ts A \teq B \kin K}
{\Gamma \ts A \tsub B \kin K}
\hspace{3em}
\infruleSimp[SK-Refl-KEq]
{\Gamma \ts J \keq K}
{\Gamma \ts J \tsub K}
\medskip
\end{center}
Another consequence of these rules is that we can treat well-typed
terms and well-kinded types up to type and kind equality,
\begin{corollary}[conversion] The following are admissible.
\end{corollary}
\begin{multicols}{2}
\typicallabel{K-Conv}

\infrule[\ruledef{K-Conv}]
{\Gamma \ts A \kin J  \andalso  \Gamma \ts J \keq K}
{\Gamma \ts A \kin K}

\infrule[\ruledef{ST-Conv}]
{\Gamma \ts A \tsub B \kin J  \andalso  \Gamma \ts J \keq K}
{\Gamma \ts A \tsub B \kin K}

\infrule[\ruledef{T-Conv}]
{\Gamma \ts t \tin A  \andalso  \Gamma \ts A \teq B \kin \kstar}
{\Gamma \ts t \tin B}

\infrule[\ruledef{TEq-Conv}]
{\Gamma \ts A \teq B \kin J  \andalso  \Gamma \ts J \keq K}
{\Gamma \ts A \teq B \kin K}
\end{multicols}

In light of their order-theoretic properties, we often call kind and
type equality judgments \emph{equations} and subkinding and subtyping
judgments \emph{inequations}.
We sometimes use equational reasoning notation in proofs, \ie we write
\[
\Gamma \; \ts \; A_1 \; \teq \; A_2 \; \teq \; \cdots \; \teq \; A_i
\; \tsub \; A_{i+1} \; \tsub \; \cdots \; \teq \; A_n \; \alEq \;
A_{n+1} \; \alEq \; \cdots \; \teq \; A_m \; \kin \; K
\]
to denote chains of (in)equations where the use of the corresponding
transitivity rules is left implicit.
In so doing, we may freely mix the relations $\tsub$, $\teq$ and
$\alEq$ provided that they are defined on the same sort (\ie kinds or
Such chains are always interpreted as judgments of the weakest
relation they contain.

\subsection{Validity of the Declarative System}
\label{sec:decl_validity_full}

In this section, we state and prove a number of \emph{validity
properties} for the various judgments defined in
\Fig[Figs.]{decl_rules1} and~\ref{fig:decl_rules2} of the paper
Roughly, we say that a judgment is valid if all its parts are
well-formed.  For example, \emph{subkinding validity} states that, if
$\Gamma \ts J \ksub K$, then both $J$ and $K$ are actually well-formed
kinds.  We saw another example earlier: \emph{context
validity}~(\Lem{decl_ctx_valid}) states that the context $\Gamma$ of
any judgment $\judgD{\Gamma}$ is well-formed.  Here is a summary of
the validity properties that remain to be proven.

\begin{lemma}[validity]\label{lem:decl_validity_full}
The judgments defined in \Fig[Figs.]{decl_rules1}
and~\ref{fig:decl_rules2} enjoy the following validity properties.
\begin{enumerate}[nosep,leftmargin=11.5em,labelsep=1em,topsep=1ex]
\item[(kinding validity)]
If $\; \Gamma \ts A \kin K$, then $\kindD{\Gamma}{K}$.

\item[(typing validity)]
If $\; \Gamma \ts t \tin A$, then $\typeD{\Gamma}{A}$.

\item[(subkinding validity)]
If $\; \Gamma \ts J \ksub K$, then $\kindD{\Gamma}{J}$ and

\item[(subtyping validity)]
If $\; \Gamma \ts A \tsub B \kin K$, then $\Gamma \ts A \kin K$ and
$\Gamma \ts B \kin K$.

\item[(kind equation validity)]
If $\; \Gamma \ts J \keq K$, then $\kindD{\Gamma}{J}$ and

\item[(type equation validity)]
If $\; \Gamma \ts A \teq B \kin K$, then $\Gamma \ts A \kin K$ and
$\Gamma \ts B \kin K$.
\end{enumerate}
\end{lemma}
These validity properties provide a ``sanity check'' for the static
semantics developed in this section, but they also play a crucial role
in the proofs of other important properties, such as subject
reduction, soundness of type normalization and and type safety.

Unfortunately, the validity properties are harder to prove than one
might expect.  The proofs of kinding, subkinding and subtyping
validity require the following \emph{functionality} lemma for
the case of \ruleref{ST-App}.
\begin{lemma}[functionality]\label{lem:decl_funct_full}
Let $\Gamma \ts A_1 \teq A_2 \kin K$.
\begin{enumerate}
\item If $\; \kindD{\Gamma, X \kas K, \Delta}{J}$, then
$\Gamma, \subst{\Delta}{X}{A_1} \ts \subst{J}{X}{A_1} \keq
\subst{J}{X}{A_2}$.
\item If $\; \Gamma, X \kas K, \Delta \ts B \kin J$, then
$\Gamma, \subst{\Delta}{X}{A_1} \ts \subst{B}{X}{A_1} \keq
\subst{B}{X}{A_2} \kin \subst{J}{X}{A_1}$.
\end{enumerate}
\end{lemma}
But a naive attempt at proving this lemma directly leads to a circular
dependency on kinding and subtyping validity, in a way that is not
easily resolved.
In particular, it is not sufficient to simply prove the two statements

It is instructive to play through the critical cases encountered when
attempting to prove \Lem[Lemmas]{decl_validity_full}
and~\ref{lem:decl_funct_full} directly to see where things go wrong
and to better understand the solution described in the next section.
We start with subtyping validity, attempting a proof by induction on
subtyping derivations.  For the case of the application
rule~\ruleref{ST-App}, we are given
$\Gamma \ts A_1 \tsub A_2 \kin \dfun{X}{J}{K}$ and
$\Gamma \ts B_1 \teq B_2 \kin J$, and we would like to show that
$\Gamma \ts \app{A_1}{B_1} \kin \subst{K}{X}{B_1}$ and
$\Gamma \ts \app{A_2}{B_2} \kin \subst{K}{X}{B_1}$.  We can already
spot the source of trouble: the type $B_1$ that is being substituted
for $X$ in the kind of the second type application differs from the
argument type $B_2$.  By the IH, we get
$\Gamma \ts A_2 \kin \dfun{X}{J}{K}$ and $\Gamma \ts B_2 \kin J$, and
applying~\ruleref{K-App} we obtain
$\Gamma \ts \app{A_2}{B_2} \kin \subst{K}{X}{B_2}$ but, as expected,
the kinds do not match up.  If we could show that
$\Gamma \ts \subst{K}{X}{B_2} \keq \subst{K}{X}{B_1}$, then
by~\ruleref{K-Conv}, we would be done.  Enter functionality of kind

For the functionality lemma, we attempt a proof by simultaneous
induction on kind formation and kinding derivations and consider the
case where the current kinding derivation ends in an instance of the
operator abstraction rule~\ruleref{K-Abs}.  In addition to the premise
$\Gamma \ts B_1 \teq B_2 \kin J$, we are given derivations for
$\kindD{\Gamma, X \kas J}{K_1}$ and
$\Gamma, X \kas J, Y \kas K_1 \ts A \kin K_2$, and we want to show
\[
\Gamma \ts \; \subst{(\lam{Y}{K_1}{A})}{X}{B_1} \; \teq \;
\subst{(\lam{Y}{K_1}{A})}{X}{B_2} \; \kin \;
\subst{(\dfun{Y}{K_1}{K_2})}{X}{B_1}.
\]
To do so, we would like to use the rule~\ruleref{ST-Abs} together
with~\ruleref{ST-AntiSym} but we first need to establish the
right-hand validity of the above equation, \ie that
\[
\Gamma \ts \subst{(\lam{Y}{K_1}{A})}{X}{B_2} \kin
\subst{(\dfun{Y}{K_1}{K_2})}{X}{B_1}.
\]
Clearly, \Lem{decl_validity_full} would be helpful here: equation
validity would give us $\Gamma \ts B_2 \kin J$, from which we could
$\Gamma \ts \subst{(\lam{Y}{K_1}{A})}{X}{B_2} \kin
\subst{(\dfun{Y}{K_1}{K_2})}{X}{B_2}$ by~\Lem{decl_subst}.  This is
almost what we need.  Again, we face a mismatch in kinds that could,
in principle, be remedied by using functionality of kind formation
together with~\ruleref{K-Conv}.  Concretely, we would like to invoke
the IH to derive
$\Gamma \ts \subst{(\dfun{Y}{K_1}{K_2})}{X}{B_1} \keq
\subst{(\dfun{Y}{K_1}{K_2})}{X}{B_2}$.  Alas, we do not have a
suitable sub-derivation to do so.  Although
$\kindD{\Gamma}{\dfun{Y}{K_1}{K_2}}$ follows from kinding validity, we
cannot apply the IH to this result because it is not a
sub-derivation of our overall premise.  Indeed, none of the
sub-derivations we are given are sufficient to derive the required
kind equation.

Note that we could finish the proof of this case if only (1)~the
rule~\ruleref{K-Abs} had an additional premise
$\kind{\Gamma, X \kas J, Y \kas K_1}{K_2}$ and (2)~the IH was a bit
stronger, so that we could use it to derive
\[
\Gamma, Y \kas \subst{K_1}{X}{B_1} \ts \subst{K_2}{X}{B_1} \keq
\subst{K_2}{X}{B_2}.
\]
This, together with a similar use of the IH on the first premise
of~\ruleref{ST-Abs} and some uses of \Lem{decl_subst},
\ruleref{ST-Refl-TEq} and~\ruleref{SK-DArr}, would be enough to derive
$\Gamma \ts \subst{(\dfun{Y}{K_1}{K_2})}{X}{B_2} \ksub
\subst{(\dfun{Y}{K_1}{K_2})}{X}{B_1}$,
which we could then put to use with~\ruleref{K-Sub}.  Indeed, these
are the basic ideas that will allow us to resolve the circular
dependency between~\Lem{decl_validity_full} and~\Lem{decl_funct_full}.
We start by addressing point~(1).

\subsubsection{The Extended System}

We define a pair of \emph{extended} kinding and subtyping judgments
where some rules have been endowed with additional premises.
These are precisely the premises highlighted in gray in
\Fig[Figs.]{decl_rules1} and~\ref{fig:decl_rules2}.
We call these extra premises \emph{validity conditions}.
Crucially, the validity conditions of an extended rule are redundant
in the sense that they follow (more or less) directly from the
remaining premises of the rule via \Lem{decl_validity_full}.
For example, the extended rule~\ruleref{K-Abs} carries the extra
premise $\kindD{\Gamma, X \kas J}{K}$ which follows directly from
applying kinding validity to the rule's second premise
$\Gamma, X \kas J \ts A \kin K$.  Thanks to this invariant, the two
sets of rules are in fact equivalent -- every derivation of an
extended kinding or subtyping judgment has a corresponding derivation
that uses only original rules, and vice-versa.  We give a formal
equivalence proof in \Sec{decl_equivalence}.

Since kinding and subkinding are defined mutually with all the other
judgments of the declarative system (except typing), the extension
indirectly affects those judgments as well.  We call the entire set of
extended judgments the \emph{extended (declarative) system}, as
opposed to the \emph{original (declarative) system}.  We will
sometimes distinguish the two systems by writing $\judgDD{\Gamma}$ for
judgments of the original system and $\judgEE{\Gamma}$ for those of
the extended system.  Since the two systems are equivalent, this
distinction only matters in a few key situations -- notably the
development in the remainder of this section.  When we refer to the
``declarative system'' in the following sections, we will always mean
the original declarative system, unless otherwise noted.

The idea of extending a set of inference rules with redundant premises
in order to simplify metatheoretic proofs is not new.
For example, \citet{HarperP05tocl} use similar premises to establish
validity properties for the typing judgments of a variant of LF.
Furthermore, some readers will have noticed that a few of the original
declarative rules already carry redundant premises.  For example, the
first premise $\kindD{\Gamma}{J}$ of the rule \ruleref{K-Abs} could
easily be reconstructed from its second premise
$\Gamma, X \kas J \ts A \kin K$ via context validity
(\Lem{decl_ctx_valid}).  The rules~\ruleref{Wf-DArr}, \ruleref{K-All},
\ruleref{T-Abs}, and~\ruleref{T-TAbs} carry similar validity
conditions.  We include these premises primarily because their
presence simplifies the proof of the substitution lemma
(\Lem{decl_subst}).  Context validity, on the other hand, remains
easily provable without them.

To prove the validity properties stated in~\Lem{decl_validity_full}
for both the original and extended systems, we use the following
\begin{enumerate}
\item\label{item:val-s1} prove that the validity properties hold for the
extended judgments;

\item prove that the two systems are equivalent, \ie that
\begin{enumerate}
\item the extended rules are \emph{sound} \wrt to the original
ones --~we can drop the validity conditions without affecting the
conclusions of any derivations~-- and that
\item the extended rules are \emph{complete} \wrt to the original
ones -- the additional validity conditions follow from the remaining
premises of the extended rules via the validity properties proved
in step~\Item{val-s1};
\end{enumerate}

\item prove that the validity properties hold for the original system
via the equivalence -- convert original derivations to extended
derivations (via completeness), derive the property in question,
convert the conclusion back (via soundness).
\end{enumerate}

Before we continue, we should point out that some of the validity
conditions of the extended system are not actually necessary for the
proof of~\Lem[Lemmas]{decl_validity_full}
and~\ref{lem:decl_funct_full} -- some even complicate the proofs.
However, we will face a similar cyclic dependency later on when
attempting to prove the equivalence of the (original) declarative
system and the \emph{canonical system} of judgments introduced
in~\Sec{canonical}.  Rather than introducing yet another extension to
the declarative system later, we opt for a combined system containing
all of the extra conditions.

We start the development set out above by noting that all the basic
metatheoretic properties established in \Sec{decl_basics} still hold
for the extended system.  The proofs carry over with minor adjustments
to deal with the additional premises.
Next, we prove a variant of the functionality lemma discussed above
but using the extended kinding and subtyping rules.
To do so, we need the following auxiliary definition of \emph{context
equality} and an associated corollary of context weakening.
\begin{center}
\infruleSimp{\quad}{\ctxEqD{\cempty}{\cempty}}
\hspace{3em}
\infruleSimp
{\ctxEqD{\Gamma}{\Delta} \andalso \Gamma \ts J \keq K}
{\ctxEqD{\Gamma, X \kas J}{\Delta, X \kas K}}
\hspace{3em}
\infruleSimp
{\ctxEqD{\Gamma}{\Delta} \andalso \Gamma \ts A \teq B \kin \kstar}
{\ctxEqD{\Gamma, x \tas A}{\Delta, x \tas B}}
\end{center}
\begin{corollary}[context conversion]\label{cor:decl_ctx_conv}
If $\; \ctxD{\Gamma}$ and $\ctxEqD{\Gamma}{\Delta}$ and $\judgD{\Delta}$,
then $\judgD{\Gamma}$.
\end{corollary}
Context equality $\ctxEqD{\Gamma}{\Delta}$ is simply the pointwise
lifting of type and kind equality to contexts.
It allows us to relate the bindings appearing in two syntactically
different contexts $\Gamma$ and $\Delta$, as illustrated in our
extended functionality lemma.
\begin{lemma}[functionality -- extended version]
\label{lem:decl_funct_ext}
Substitutions of equal types in well-formed expressions result in
well-formed equations.  Let $\Gamma$, $\Delta$, $\Sigma$ be
contexts, $K$ a kind and $A_1$, $A_2$ types, such that
$\Gamma \ts A_1 \kin K$ and $\Gamma \ts A_2 \kin K$, the context
$\Gamma, \Sigma$ is well-formed and the following equations hold:
\begin{align*}
&\Gamma \ts A_1 \; \teq \; A_2 \kin K
&&\ctxD{\Gamma, \Sigma \; \keq \; \Gamma, \subst{\Delta}{X}{A_1}}
&&\ctxD{\Gamma, \Sigma \; \keq \; \Gamma, \subst{\Delta}{X}{A_2}}.
\end{align*}
\begin{enumerate}
\item If $\; \kindD{\Gamma, X \kas K, \Delta}{J}$, then
$\Gamma, \Sigma \ts \subst{J}{X}{A_1} \keq \subst{J}{X}{A_2}$.
\item If $\; \Gamma, X \kas K, \Delta \ts B \kin J$, then
$\Gamma, \Sigma \ts \subst{B}{X}{A_1} \keq \subst{B}{X}{A_2} \kin
\subst{J}{X}{A_1}$.
\end{enumerate}
\end{lemma}
Compared to \Lem{decl_funct_full}, the lemma has been strengthened
--~so that it is applicable to any type variable binding in a context,
not just the last one~-- and simultaneously weakened -- by adding
extra conditions on $A_1$, $A_2$ and the target context
$\Gamma, \Sigma$.
The latter are effectively validity conditions ensuring that the proof
of the lemma does not depend on \Lem{decl_validity_full}.
The separate target context~$\Sigma$ is used to symmetrize the
treatment of context extensions, which is helpful when dealing with
kind annotations in contravariant positions.
\begin{proof}
The two parts are proven simultaneously, by induction on extended
kind formation and kinding derivations, respectively.  The proof of
the first part is relatively straightforward, while the proof of
the second part deserves some attention.  We present a few key
cases, the others are similar.
\begin{itemize}
\item \emph{Case~\ruleref{K-Var}.} We have $B = Y$, $J = \Gamma(Y)$
and $\ctxD{\Gamma, X \kas K, \Delta}$.  We distinguish two cases
based on $Y$.
\begin{itemize}
\item \emph{Sub-case $Y = X$.}  We have
$J = K \alEq \subst{K}{X}{A_1}$ since $X \notin \fv(K)$.  By
iterated weakening, we get
$\Gamma, \Sigma \ts A_1 \teq A_2 \kin \subst{K}{X}{A_1}$ and we
are done.
\item \emph{Sub-case $Y \neq X$.}  We have
$(\Gamma, \subst{\Delta}{X}{A_1})(Y) \alEq \subst{J}{X}{A_1}$,
either because $Y \in \dom(\Gamma)$ and $X \notin \fv(J)$, or
because $Y \in \dom(\Delta)$ and
$(\subst{\Delta}{X}{A_1})(Y) = \subst{J}{X}{A_1}$.  Furthermore,
since $\ctxEqD{\Gamma, \Sigma}{\Gamma, \subst{\Delta}{X}{A_1}}$
we have
\[
\Gamma, \Sigma \; \ts \; (\Gamma, \Sigma)(Y) \; \keq
\; (\Gamma, \subst{\Delta}{X}{A_1})(Y) \; \alEq \;
\subst{J}{X}{A_1}.
\]
We conclude by~\ruleref{K-Var}, \ruleref{K-Conv},
\end{itemize}

\item \emph{Case~\ruleref{K-All}.} We have $B = \all{Y}{J_1}{B_1}$
and $J = \kstar$ for some kind $J_1$ and type $B_1$, as well as
$\kindD{\Gamma, X \kas K, \Delta}{J_1}$ and
$\typeD{\Gamma, X \kas K, \Delta, Y \kas J_1}{B_1}$.  We want to
show that $\subst{(\all{Y}{J_1}{B_1})}{X}{A_1}$ and
$\subst{(\all{Y}{J_1}{B_1})}{X}{A_2}$ are mutual subtypes.  To do
so, we first prove that
\begin{alignat*}{2}
&\typeD{\Gamma, \Sigma \;}{\; \subst{(\all{Y}{J_1}{B_1})}{X}{A_1} \;}
&& \quad
\typeD{\Gamma, \Sigma \;}{\; \subst{(\all{Y}{J_1}{B_1})}{X}{A_2} \;}\\
&\Gamma, \Sigma \; \ts \; \subst{J_1}{X}{A_2} \; \ksub \;
\subst{J_1}{X}{A_1} && \quad
\Gamma, \Sigma \; \ts \; \subst{J_1}{X}{A_1} \; \ksub \;
\subst{J_1}{X}{A_2} \\
&\Gamma, \Sigma, X \kas \subst{J_1}{X}{A_2} \; \ts \;
\subst{B_1}{X}{A_1} \; \tsub \; \subst{B_1}{&&X}{A_2} \; \kin \;
\kstar \\
&\Gamma, \Sigma, X \kas \subst{J_1}{X}{A_1} \; \ts \;
\subst{B_1}{X}{A_2} \; \tsub \; \subst{B_1}{&&X}{A_1} \; \kin \;
\kstar
\end{alignat*}
then apply~\ruleref{ST-All} twice, and conclude
with~\ruleref{ST-AntiSym}.  The two kinding judgments follow from
the premises by the substitution lemma~(\Lem{decl_subst}), the two
subkinding judgments by the IH.  The last two subtyping judgments
require some extra work.

Note that the additional type variable bindings in the two
judgments differ syntactically, so we will have to use the IH
twice, with different target contexts.  In each case we need to
show that the kind of the additional binding is well-formed and
equal to $\subst{J_1}{X}{A_1}$ and $\subst{J_1}{X}{A_2}$,
respectively.  Concretely, we need to show that
\begin{gather*}
\kindD{\Gamma, \Sigma}{ \subst{J_1}{X}{A_2} \keq \subst{J_1}{X}{A_1}}
\hspace{4em} \kindD{\Gamma, \Sigma}{\subst{J_1}{X}{A_2}} \\
\kindD{\Gamma, \Sigma}{ \subst{J_1}{X}{A_2} \keq \subst{J_1}{X}{A_2}}
\end{gather*}
for the first invocation of the IH, and three analogous statements
for the second.  The first equation follows from the two
subkinding judgments above via~\ruleref{ST-AntiSym}.  The context
formation judgment and the first equation follow from the
substitution lemma and~\ruleref{TEq-Refl}.  This is sufficient to
apply the IH and obtain the first of the two remaining subtyping
judgments via~\ruleref{ST-Refl-TEq}.  The proof of the second one
is similar.

\item \emph{Case~\ruleref{K-App}.} We have $B = \app{B_1}{B_2}$
and $J = \subst{J_2}{Y}{B_2}$ for some $B_1$, $B_2$, $J_2$, as
well as
\begin{align*}
&\Gamma \ts A_1 \kin K, && \Gamma \ts A_2 \kin K \\
&\Gamma \ts A_1 \teq A_2 \kin K, && \ctxD{\Gamma, \Sigma} \\
&\ctxD{\Gamma, \Sigma \keq \Gamma, \subst{\Delta}{X}{A_1}}, &
&\ctxD{\Gamma, \Sigma \keq \Gamma, \subst{\Delta}{X}{A_2}}, \\
&\Gamma, X \kas K, \Delta \ts B_1 \kin \dfun{Y}{J_1}{J_2}, &
&\Gamma, X \kas K, \Delta \ts B_2 \kin J_1, \\
&\kindD{\Gamma, X \kas K, \Delta, Y \kas J_1}{J_2}, &
&\kindD{\Gamma, X \kas K, \Delta}{\subst{J_2}{Y}{B_2}}
\end{align*}
for some $J_1$.  We want to establish that that
$\subst{(\app{B_1}{B_2})}{X}{A_1}$ and
$\subst{(\app{B_1}{B_2})}{X}{A_2}$ are mutual subtypes in
$\subst{\subst{J_2}{Y}{B_2}}{X}{A_1}$, \ie that
\begin{align}
&\Gamma, \Sigma \; \ts \; \subst{(\app{B_1}{B_2})}{X}{A_1} \; \tsub \;
\subst{(\app{B_1}{B_2})}{X}{A_2} \; \kin \;
\subst{\subst{J_2}{Y}{B_2}}{X}{A_1}, \quad \text{and}
\label{eq:funct1}\\
& \Gamma, \Sigma \; \ts \; \subst{(\app{B_1}{B_2})}{X}{A_2}
\; \tsub \; \subst{(\app{B_1}{B_2})}{X}{A_1} \; \kin \;
\subst{\subst{J_2}{Y}{B_2}}{X}{A_1}.\label{eq:funct2}
\end{align}

The first half is fairly straightforward.  Applying the IH to the
first two premises of~\ruleref{K-App} yields
corresponding equations, the first of which we turn into an
inequation via~\ruleref{ST-Refl-TEq}.
\begin{align*}
&\Gamma, \Sigma \; \ts \; \subst{B_1}{X}{A_1} \; \tsub \;
\subst{B_1}{X}{A_2} \; \kin \; \subst{(\dfun{Y}{J_1}{J_2})}{X}{A_1},\\
&\Gamma, \Sigma \; \ts \; \subst{B_2}{X}{A_1} \; \teq \;
\subst{B_2}{X}{A_2} \; \kin \; \subst{J_1}{X}{A_1}.
\end{align*}

In order to apply~\ruleref{ST-App} we also need to derive the
following validity conditions:
\begin{align*}
& \Gamma, \Sigma \ts \subst{B_2}{X}{A_1} \kin \subst{J_1}{X}{A_1}, &&
\kindD{\Gamma, \Sigma, Y \kas \subst{J_1}{X}{A_1}}{
\subst{J_2}{X}{A_1}}, \\
& \kindD{\Gamma, \Sigma}{
\subst{\subst{J_2}{X}{A_1}}{Y}{\subst{B_2}{X}{A_1}}}.
\end{align*}
All three follow from premises of~\ruleref{K-App} and the
substitution lemma~(\Lem{decl_subst}), followed by a use
of~\Cor{decl_ctx_conv} to adjust the contexts.  Adjusting the
context of
$\kindD{\Gamma, \subst{\Delta}{X}{A_1}, Y \kas
\subst{J_1}{X}{A_1}}{ \subst{J_2}{X}{A_1}}$,
requires a bit more work because we need to prove that the kind of
the extra binding $Y \kas \subst{J_1}{X}{A_1}$ is well-formed.  To
do so, we first invoke context validity~(\Lem{decl_ctx_valid}) on
the second validity condition of~\ruleref{K-App}, which gives
us $\kindD{\Gamma, X \kas K, \Delta}{J_1}$.  Form this, we derive
the desired well-formedness proof via the substitution lemma.
By~\ruleref{ST-App} and~\Lem{sub_commutes}, we arrive

We have to work a bit harder to prove~\eqref{eq:funct2}.
Again, we want to apply~\ruleref{ST-App}, and again, the first
two premises follow from the IH --~this time followed by a use
of~\ruleref{TEq-Sym} to adjust the direction~--
and~\ruleref{ST-Refl-TEq} to turn the first equation into a
subtyping statement.  The validity conditions are
\begin{align*}
& \Gamma, \Sigma \ts \subst{B_2}{X}{A_2} \kin \subst{J_1}{X}{A_1}, &&
\kindD{\Gamma, \Sigma, Y \kas \subst{J_1}{X}{A_1}}{
\subst{J_2}{X}{A_1}}, \\
& \kindD{\Gamma, \Sigma}{
\subst{\subst{J_2}{X}{A_1}}{Y}{\subst{B_2}{X}{A_2}}}.
\end{align*}
We have already established the second condition; the third one
follows from applying the substitution lemma to the first two.  So
it remains to prove the first.

We start by deriving
$\Gamma, \Sigma \ts \subst{B_2}{X}{A_2} \kin \subst{J_1}{X}{A_2}$
via the substitution lemma and context conversion.  Next, we would
like to use the IH to show that
$\Gamma, \Sigma \ts \subst{J_1}{X}{A_2} \keq \subst{J_1}{X}{A_1}$
in order to adjust the kind of the previous judgment
via~\ruleref{K-Conv}.  But to do so, we need to find a derivation
of $\kindD{\Gamma, X \kas K, \Delta}{J_1}$ that is a strict
sub-derivation of our current instance of \ruleref{K-App}.

Fortunately, this is always possible, thanks to the validity
condition $\kindD{\Gamma, X \kas K, \Delta, Y \kas J_1}{J_2}$.
Since the contexts of kind formation judgments are always
well-formed themselves (see~\Lem{decl_ctx_valid}), it suffices to
traverse the derivation tree of this judgment upwards along kind
formation and kinding rules until one arrives at a ``leaf'' --~an
instance of~\ruleref{K-Var}, \ruleref{K-Top} or~\ruleref{K-Bot}~--
which holds a well-formedness derivation for the current context.
That context formation derivation, in turn, contains a
sub-derivation of the desired kind formation judgment.  Readers
who are skeptical of this somewhat informal argument are
encouraged to state and prove a helper lemma that combines the IH
with the ``lookup procedure'' just described.  The lemma is proven
simultaneously with the main lemma, by induction on kind formation
and kinding derivations.

With all the validity conditions in place, we
apply~\ruleref{ST-App} to obtain
\[
\Gamma, \Sigma \; \ts \; \subst{(\app{B_1}{B_2})}{X}{A_2} \;
\tsub \; \subst{(\app{B_1}{B_2})}{X}{A_1} \; \kin \;
\subst{\subst{J_2}{X}{A_1}}{Y}{\subst{B_2}{X}{A_2}}.
\]
To complete the proof of~\ref{eq:funct2}, we
use~\ruleref{ST-Conv} and
\begin{align*}
\Gamma, \Sigma &{} \; \ts \;
\subst{\subst{J_2}{X}{A_1}}{Y}{\subst{B_2}{X}{A_2}}\\
&{} \; \keq \;
\subst{\subst{J_2}{X}{A_2}}{Y}{\subst{B_2}{X}{A_2}}
\tag{by~\Lem{decl_subst}}\\
&{} \; \alEq \;
\subst{\subst{J_2}{Y}{B_2}}{X}{A_2} \tag{by~\Lem{sub_commutes}}\\
&{} \; \keq \;
\subst{\subst{J_2}{Y}{B_2}}{X}{A_1} \tag{by the IH}
\end{align*}
using our earlier result
$\Gamma, \Sigma \ts \subst{J_1}{X}{A_2} \keq \subst{J_1}{X}{A_1}$
in the first step and the final validity condition
of~\ruleref{K-App} in the last.  \qedhere

\end{itemize}
\end{proof}

We are now ready to prove~\Lem{decl_validity_full} in the extended
system, simultaneously with the following lemma.
\begin{lemma}\label{lem:ST-Intv-Star}
Subtypes inhabiting interval kinds are proper subtypes.  If
$\; \Gamma \ts A \tsub B \kin C \intv D$, then also
$\Gamma \ts A \tsub B \kin \kstar$.
\end{lemma}
\begin{proof}[Proof of \Lem{decl_validity_full} and
\Lem{ST-Intv-Star} -- extended version]\label{pf:decl_validity_ext}
All the validity properties are proven simultaneously with
\Lem{ST-Intv-Star}, by induction on the derivations of the
respective premises.  The proof is now mostly routine, thanks to the
validity conditions.  The only interesting cases are those of
of~\ruleref{ST-App}, where we use the functionality lemma to adjust
the kind of the right-hand validity proof, and~\ruleref{ST-Intv},
where we use~\Lem{ST-Intv-Star}.  The proof of \Lem{ST-Intv-Star}
uses subtyping validity in turn.
\end{proof}

\begin{corollary}\label{lem:TEq-Intv-Star}
Equal types in intervals are equal as proper types.  If
$\; \Gamma \ts A \teq B \kin C \intv D$, then also
$\Gamma \ts A \teq B \kin \kstar$.
\end{corollary}

\subsubsection{Equivalence}
\label{sec:decl_equivalence}

The next and final step in our program for
proving~\Lem{decl_validity_full} is to establish the equivalence of
the two declarative systems.
\begin{lemma}\label{decl_equiv}
The original and extended declarative systems are equivalent:
$\judgDD{\Gamma}$ iff\, $\judgEE{\Gamma}$.
\end{lemma}

Thanks to this equivalence, all the validity properties laid out
in~\Lem{decl_validity_full} also hold for the original judgments of
the declarative system.
Our original functionality lemma (\Lem{decl_funct_full}) and the
following strengthened version of \Lem{decl_weak_narrow} follow as
corollaries of validity and \Lem[Lemmas]{decl_funct_ext} and
\ref{lem:decl_weak_narrow}, respectively.
\begin{corollary}[context narrowing -- strong version]
\label{cor:decl_narrow}
\begin{enumerate}
\item If $\; \Gamma \ts A \tsub B \kin \kstar$
and $\judgD{\Gamma, x \tas B, \Delta}$, then
$\judgD{\Gamma, x \tas A, \Delta}$.
\item If $\; \Gamma \ts J \ksub K$ and
$\judgD{\Gamma, X \kas K, \Delta}$, then
$\judgD{\Gamma, X \kas J, \Delta}$,
\end{enumerate}
\end{corollary}

\subsection{Admissible Congruence Rules for Type and Kind Equality}
\label{sec:decl_cong}

Thanks to the validity properties established in
\Sec{decl_validity_full},
we are able to prove a number of admissible \emph{congruence rules}
for kind and type equality.
These follow the same structure as the corresponding subkinding and
subtyping rules but are generally a bit simpler.
First, we no longer need to pay attention to the variance (or
polarity) of constructor arguments because equality is symmetric.
Second, the left-hand validity conditions present in the
rules~\ruleref{SK-DArr} and~\ruleref{ST-All} become redundant in the
corresponding equality rules because the kind annotations in the left-
and right-hand sides are convertible.
Finally, thanks to symmetry, only one rule is needed for
$\beta$-conversion, and likewise for $\eta$-conversion.
\begin{lemma}\label{lem:keq_cong}
Kind equality is a congruence with respect to the interval and
dependent arrow kind formers, \ie the following kind equality
rules are admissible.
\end{lemma}
\begin{multicols}{2}
\infrule[\ruledef{KEq-Intv}]
{\Gamma \ts A_1 \teq A_2 \kin \kstar  \andalso
\Gamma \ts B_1 \teq B_2 \kin \kstar}
{\Gamma \ts A_1 \intv B_1 \keq A_2 \intv B_2}

\infrule[\ruledef{KEq-DArr}]
{\Gamma \ts J_1 \keq J_2  \andalso
\Gamma, X \kas J_1 \ts K_1 \keq K_2}
{\Gamma \ts \dfun{X}{J_1}{K_1} \keq \dfun{X}{J_2}{K_2}}
\end{multicols}

\begin{lemma}\label{lem:teq_cong}
Type equality is a congruence with respect to the various type
formers and includes $\beta$~and $\eta$-conversion, \ie the
following type equality rules are admissible.
\end{lemma}
\begin{multicols}{2}
\infrule[\ruledef{TEq-All}]
{\Gamma \ts K_1 \keq K_2  \andalso
\Gamma, X \kas K_1 \ts A_1 \teq A_2 \kin \kstar}
{\Gamma \ts \all{X}{K_1}{A_1} \teq \all{X}{K_2}{A_2} \kin \kstar}

\infrule[\ruledef{TEq-Arr}]
{\Gamma \ts A_1 \teq A_2 \kin \kstar  \andalso
\Gamma \ts B_1 \teq B_2 \kin \kstar}
{\Gamma \ts \fun{A_1}{B_1} \teq \fun{A_2}{B_2} \kin \kstar}

\infrule[\ruledef{TEq-Abs}]
{\Gamma \ts \lam{X}{J_1}{A_1} \kin \dfun{X}{J}{K}\\
\Gamma \ts \lam{X}{J_2}{A_2} \kin \dfun{X}{J}{K}\\
\Gamma, X \kas J \ts A_1 \teq A_2 \kin K}
{\Gamma \ts \lam{X}{J_1}{A_1} \teq \lam{X}{J_2}{A_2} \kin \dfun{X}{J}{K}}
\end{multicols}
\begin{multicols}{2}
\infrule[\ruledef{TEq-App}]
{\Gamma \ts A_1 \teq A_2 \kin \dfun{X}{J}{K}  \andalso
\Gamma \ts B_1 \teq B_2 \kin J}
{\Gamma \ts \app{A_1}{B_1} \teq \app{A_2}{B_2} \kin \subst{K}{X}{B_1}}

\infrule[\ruledef{TEq-Sing}]
{\Gamma \ts A_1 \teq A_2 \kin B \intv C}
{\Gamma \ts A_1 \teq A_2 \kin A_1 \intv A_1}
\end{multicols}
\begin{multicols}{2}
\infrule[\ruledefN{TEq-Beta}{TEq-$\beta$}]
{\Gamma, X \kas J \ts A \kin K  \andalso  \Gamma \ts B \kin J}
{\Gamma \ts \app{(\lam{X}{J}{A})}{B} \teq \subst{A}{X}{B} \kin
\subst{K}{X}{B}}

\infrule[\ruledefN{TEq-Eta}{TEq-$\eta$}]
{\Gamma \ts A \kin \dfun{X}{J}{K}  \andalso  X \notin \fv(A)}
{\Gamma \ts \lam{X}{J}{\app{A}{X}} \teq A \kin \dfun{X}{J}{K}}
\end{multicols}
\begin{proof}
The admissibility proofs of the above rules all follow the same
basic pattern.
We want to show that the left- and right-hand sides of the
conclusions are mutual subkinds or subtypes, respectively.
To do so, we employ the respective subkinding and subtyping rules,
adjusting the kinds of additional bindings and subtyping judgments
using context narrowing (\Cor{decl_narrow}),
subsumption~\ruleref{ST-Sub}, conversion~\ruleref{ST-Conv} and
functionality~(\Lem{decl_funct}) where necessary.
When additional validity properties are required,
\Lem{decl_validity} delivers the required well-formedness or
well-kindedness proofs.

For example, the proof of \ruleref{TEq-Sing} proceeds as follows.
We note that the premise must have been derived using
\ruleref{ST-AntiSym}, hence we have
$\Gamma \ts A_1 \tsub A_2 \kin B \intv C$ and
$\Gamma \ts A_2 \tsub A_1 \kin B \intv C$.
By~\ruleref{ST-Intv}, \Lem{ST-Intv-Star} and subtyping validity
\begin{align*}
&\Gamma \ts A_1 \tsub A_2 \kin A_1 \intv A_2 \quad \text{(1a)} &
&\Gamma \ts A_1 \tsub A_2 \kin \kstar \quad \text{(1b)} &
&\Gamma \ts A_1 \kin \kstar \quad \text{(1c)} \\
&\Gamma \ts A_2 \tsub A_1 \kin A_2 \intv A_1 \quad \text{(2a)} &
&\Gamma \ts A_2 \tsub A_1 \kin \kstar \quad \text{(2b)} &
&\Gamma \ts A_2 \kin \kstar \quad \text{(2c)}
\end{align*}
From (1a), (1c) and (2b) we derive
\begin{prooftree}
\AxiomC{$\Gamma \ts A_1 \tsub A_2 \kin A_1 \intv A_2$}
\AxiomC{$\Gamma \ts A_1 \kin \kstar$}
\LeftLabel{\rulerefP{ST-Refl}}
\UnaryInfC{$\Gamma \ts A_1 \tsub A_1 \kin \kstar$}
\AxiomC{$\Gamma \ts A_2 \tsub A_1 \kin \kstar$}
\RightLabel{\rulerefP{SK-Intv}}
\BinaryInfC{$\Gamma \ts A_1 \intv A_2 \ksub A_1 \intv A_1$}
\RightLabel{\rulerefP{ST-Sub}}
\BinaryInfC{$\Gamma \ts A_1 \tsub A_2 \kin A_1 \intv A_1$}
\end{prooftree}
and similarly $\Gamma \ts A_2 \tsub A_1 \kin A_1 \intv A_1$ from
(2a), (2b) and (1c).
We conclude with \ruleref{ST-AntiSym}.
\end{proof}

Note that the rule~\ruleref{TEq-Sing} (and by transitivity, the
rule~\ruleref{ST-Intv}) plays an important role in the proof of
subject reduction for types (\Thm{beta_red_teq}).
It is used in the case for \ruleref{K-Sing}, where it allows us to
relate $\beta$-equal types inhabiting singleton kinds.

\subsection{Admissible Rules for Higher-Order Extrema and Intervals}
\label{sec:decl_horules}

In this section, we state and prove admissible rules that justify the
encodings of higher-order extremal types and interval kinds given
in~\Sec{encodings} of the paper (page~\pageref{sec:encodings}).
Many of these rules are straightforward generalizations of the
corresponding rules for the types $\Top$, $\Bot$ and for proper type
intervals $A \intv B$.
The remaining rules and lemmas mostly deal with the family of kinds
$\kmax{K}$, which plays a crucial role in the other encodings and the
proofs of their respective properties.

We start by stating and proving a formation rule for
\begin{lemma} The kind $\kmax{K}$ is well-formed whenever $K$ is,
\ie the following is admissible.
\end{lemma}
\begin{center}
\infruleSimp[Wf-KMax]{\kindD{\Gamma}{K}}{\kindD{\Gamma}{\kmax{K}}}
\end{center}
\begin{proof}
By induction on the structure of $K$.
The base case uses~\ruleref{K-Bot}, \ruleref{K-Top}
and~\ruleref{Wf-Intv} to show that $\kstar$ is well-formed.
\end{proof}

The kind $\kmax{K}$ is a widened version of $K$, \ie the latter is
always a subkind of the former.  As a consequence, any type of kind
$K$ is also of kind $\kmax{K}$.
\begin{lemma}\label{lem:SK-KMax}
Any well-formed kind $K$ is a subkind of $\kmax{K}$.
\end{lemma}
\begin{center}
\infruleSimp[SK-KMax]
{\Gamma \ts K \ksub \kmax{K}}
\end{center}
\begin{proof}
By straightforward induction on the structure of $K$.
\end{proof}
\begin{corollary}\label{cor:K-KMax}
If $\; \Gamma \ts A \kin K$, then also $\Gamma \ts A \kin \kmax{K}$.
\end{corollary}

The following two lemmas introduce admissible kinding rules for the
higher-order extremal types, and prove that $\tmin{K}$ and $\tmax{K}$
are in fact extrema in~$\kmax{K}$, \ie they are the least and
greatest inhabitants of $\kmax{K}$, respectively.
\begin{lemma} Higher-order extremal types are well-formed if their
index kind is.
\end{lemma}
\begin{center}
\infruleSimp[K-TMax]{\kindD{\Gamma}{K}}{\Gamma \ts \tmax{K} \kin \kmax{K}}
\hspace{3em}
\infruleSimp[K-TMin]{\kindD{\Gamma}{K}}{\Gamma \ts \tmin{K} \kin \kmax{K}}
\end{center}
\begin{proof}
Separately, by induction on the structure of $K$.  The cases for
dependent arrow kinds use \ruleref{Wf-KMax}.
\end{proof}

\begin{lemma} The types $\tmax{K}$ and $\tmin{K}$ are the maximal and
minimal elements of $\kmax{K}$, respectively.
\end{lemma}
\begin{center}
\infruleSimp[ST-TMax]{\Gamma \ts A \kin K}
{\Gamma \ts A \tsub \tmax{K} \kin \kmax{K}}
\hspace{3em}
\infruleSimp[ST-TMin]{\Gamma \ts A \kin K}
{\Gamma \ts \tmin{K} \tsub A \kin \kmax{K}}
\end{center}
\begin{proof}
Separately, by induction on the structure of $K$.  \Cor{K-KMax} is
used to adjust the kind of the premises where necessary.  In the
inductive step, we use~\ruleref{ST-Abs} and the
$\eta$-rules~\rulerefN{ST-Eta1}{ST-$\eta_{1,2}$}.  For example, for
$K = \dfun{X}{K_1}{K_2}$ we have
\begin{alignat}{2}
\Gamma \; \ts \; A \; &\tsub \; \lam{X}{K_1}{\app{A}{X}}
&&\text{for $X \notin \fv(A)$}
\tag{by \rulerefN{ST-Eta2}{ST-$\eta_2$}}\\
&\tsub \; \lam{X}{K_1}{\tmax{K_2}} \tag{by the IH and~\ruleref{ST-Abs}}\\
&\alEq \; \tmax{\dfun{X}{K_1}{K_2}} &\;\; \kin \; \kmax{\dfun{X}{K_1}{K_2}}.
\tag{by definition}
\end{alignat}
\end{proof}

Having generalized the properties of the extremal types to their
higher-order counterparts, we now turn to interval kinds.  We start
with an admissible formation rule for higher-order intervals.
\begin{lemma} Higher-order interval kinds are well-formed if their
bounds are.
\end{lemma}
\begin{center}
\infruleSimp[Wf-HoIntv]
{\Gamma \ts A \kin K  \andalso  \Gamma \ts B \kin K}
{\kindD{\Gamma}{A \hointv{K} B}}
\end{center}
\begin{proof}
By induction on the structure of $K$.  The inductive step uses
kinding validity, \ruleref{K-Var} and~\ruleref{K-App} to expand the
\end{proof}

The subkinding rule~\ruleref{SK-Intv} for proper type intervals also
generalizes straightforwardly to intervals over arbitrary type
\begin{lemma} Higher-order interval kinds are widened in accordance
with their bounds.
\end{lemma}
\begin{center}
\infruleSimp[SK-HoIntv]
{\Gamma \ts A_2 \tsub A_1 \kin K  \andalso
\Gamma \ts B_1 \tsub B_2 \kin K}
{\Gamma \ts A_1 \hointv{K} B_1 \ksub A_2 \hointv{K} B_2}
\end{center}
\begin{proof}
By induction on the structure of $K$.  The inductive step uses
subtyping validity, \ruleref{K-Var}, \ruleref{TEq-Refl}
and~\ruleref{ST-App} to expand the bounds, and~\ruleref{Wf-HoIntv}
to establish well-formedness of the left-hand side.
\end{proof}

Next, we would like to prove an admissible higher-order singleton
introduction rule that generalizes~\ruleref{K-Sing}.  Ideally, we
would like to show that any well-kinded type $\Gamma \ts A \kin K$
inhabits its corresponding singleton kind
$\ksing{A}{K} = A \hointv{K} A$.
This is not necessarily true, however.
Consider the case of an operator variable
$X$ with declared type $\Gamma(X) = \fun{\kstar}{\kstar}$.  The
singleton kind corresponding to $X$ is
$\ksing{X}{\fun{\kstar}{\kstar}} = \dfun{Y}{\kstar}{\app{X}{Y} \!
\intv \app{X}{Y}}$,
so we would like to prove that
$\Gamma \ts X \kin \dfun{Y}{\kstar}{\app{X}{Y} \! \intv \app{X}{Y}}$.
Which kinding rules could we use to adjust the kind of $X$ to the
desired singleton kind?  Since~\ruleref{K-Sing} can only be applied to
proper types, our only option is to use the subsumption
rule~\ruleref{K-Sub}.  But unfortunately, the declared kind
$\fun{\kstar}{\kstar}$ of $X$ is a \emph{strict supertype} of the
singleton kind $\dfun{Y}{\kstar}{\app{X}{Y} \! \intv \app{X}{Y}}$, so
this cannot work.

We can, however, assign the desired singleton kind to the
\emph{$\eta$-expansion} of $X$, \ie to
$\lam{Y}{\kstar}{\app{X}{Y}}$.  Unlike $X$, the application
$\app{X}{Y}$ in the body of the $\eta$-expansion is a proper type, so
we can use~\ruleref{K-Sing} to narrow its kind.  The full derivation
\begin{prooftree}
\AxiomC{$\kindD{\Gamma}{\kstar}$}
\AxiomC{$\Gamma, Y \kas \kstar \ts
X \kin \fun{\kstar}{\kstar}$}
\AxiomC{$\Gamma, Y \kas \kstar \ts
Y \kin \kstar$}
\RightLabel{\rulerefP{K-App}}
\BinaryInfC{$\Gamma, Y \kas \kstar \ts
\app{X}{Y} \kin \kstar$}
\RightLabel{\rulerefP{K-Sing}}
\UnaryInfC{$\Gamma, Y \kas \kstar \ts
\app{X}{Y} \kin \app{X}{Y} \! \intv \app{X}{Y}$}
\RightLabel{\rulerefP{K-Abs}}
\BinaryInfC{$\Gamma \ts \lam{Y}{\kstar}{\app{X}{Y}} \kin
\dfun{Y}{\kstar}{\app{X}{Y} \! \intv \app{X}{Y}}$}
\end{prooftree}
This principle generalizes to arbitrary well-kinded types: the
$\eta$-expansion of a well-kinded type $\Gamma \ts A \kin K$ always
inhabits the corresponding singleton kind $\ksing{A}{K}$.

Given a type $A$, we define the \emph{weak $\eta$-expansion}
$\weakEtaExp{K}{A}$ of $A$ as $\weakEtaExp{B \intv C}{A} = A$ and
$\weakEtaExp{\dfun{X}{J}{K}}{A} =
\lam{X}{J}{\weakEtaExp{K}{\app{A}{X}}}$
where, as usual, we assume that $X \notin \fv(A)$.  We call this
expansion ``weak'' because the argument $X$ in the definition
$\lam{X}{J}{\weakEtaExp{K}{\app{A}{X}}}$ of the arrow case is not
$\eta$-expanded further.  This means that the result is not
$\eta$-long.  This is sufficient for the purpose of this section; we
will define a stronger version in the next section.

As expected, a type of kind $K$ is equal to its weak $\eta$-expansion
in $K$.
\begin{lemma}
Weak $\eta$-expansion is sound, \ie if $\; \Gamma \ts A \kin K$,
then $\Gamma \ts A \teq \weakEtaExp{K}{A} \kin K$.
\end{lemma}
\begin{proof}
By induction on the structure of $K$,
using~\rulerefN{TEq-Eta}{TEq-$\eta$} and~\ruleref{TEq-Abs} in the
inductive case.
\end{proof}
\vfill

\begin{lemma}
The $\eta$-expansions of type operators inhabit their higher-order
singleton intervals.
\begin{center}\normalfont
\infruleSimp[K-HoSing]
{\Gamma \ts A \kin K}
{\Gamma \ts \weakEtaExp{K}{A} \kin \ksing{A}{K}}
\end{center}
\end{lemma}
\begin{proof}
By induction on the structure of $K$.  The base case follows
from~\ruleref{K-Sing}, the inductive step from the usual combination
of kinding validity, \ruleref{K-Var}, \ruleref{K-App}
\end{proof}
\begin{corollary}
If $\Gamma \ts B_1 \tsub A \kin K$ and
$\Gamma \ts A \tsub B_2 \kin K$, then
$\Gamma \ts \weakEtaExp{K}{A} \kin B_1 \hointv{K} B_2$.
\end{corollary}

Having found ways to form, widen and populate higher-order intervals,
we still need a way to put their bounds to use.  To this end, we
introduce two \emph{higher-order bound projection} rules, which
generalize the corresponding rules~\rulerefN{ST-Bnd1}{ST-Bnd$_1$}
and~\rulerefN{ST-Bnd2}{ST-Bnd$_2$} for proper type intervals.
\begin{lemma}[higher-order bound projection]\label{lem:ho_bnd_proj}
Inhabitants of a higher-order interval are supertypes of its lower
bound and subtypes of its upper bound.
\end{lemma}
\begin{center}
\infruleSimpN{ST-HoBnd1}{ST-HoBnd$_1$}
{\Gamma \ts A \kin K  \andalso
\Gamma \ts B_1 \kin K \\
\Gamma \ts A \kin B_1 \hointv{K} B_2}
{\Gamma \ts B_1 \tsub A \kin K}
\hspace{3em}
\infruleSimpN{ST-HoBnd2}{ST-HoBnd$_2$}
{\Gamma \ts A \kin K  \andalso
\Gamma \ts B_2 \kin K \\
\Gamma \ts A \kin B_1 \hointv{K} B_2}
{\Gamma \ts A \tsub B_2 \kin K}
\end{center}
These rules are a bit weaker than one might expect.  In particular,
the additional premises $\Gamma \ts A \kin K$, $\Gamma \ts B_1 \kin K$
and $\Gamma \ts B_2 \kin K$, might seem redundant.  They are necessary
because we cannot, in general, invert well-formedness judgments about
higher-order intervals.  That is, $\kindD{\Gamma}{B_1 \hointv{K} B_2}$
does \emph{not} imply $\Gamma \ts B_1 \kin K$ and
$\Gamma \ts B_2 \kin K$, nor does
$\Gamma \ts A \kin B_1 \hointv{K} B_2$ imply $\Gamma \ts A \kin K$.
To see this, consider the kind $K = \Bot \hointv{\kempty} \Top$, where
$\kempty = \Top \intv \Bot$ is the empty interval (note the absurd
bounds).  The kind $K$ is well-formed and inhabited by both $\Bot$ and
$\Top$, yet clearly $\Bot, \Top$ are not inhabitants of $\kempty$.
Note that the formation rule~\ruleref{Wf-HoIntv} for higher-order
intervals is not to blame: although $K$ is well-formed, we cannot
prove this fact using~\ruleref{Wf-HoIntv}.  There are simply more
well-formed higher-order intervals than can be derived
\begin{proof}[Proof of \Lem{ho_bnd_proj}]
Separately, by induction on the structure of $K$.  In the base case,
we use the interval projection
rules~\rulerefN{ST-Bnd1}{ST-Bnd$_{1, 2}$} as well
as~\ruleref{ST-Intv} and~\ruleref{ST-Sub} to adjust the kinds of the
resulting inequations.  In the inductive step, we
use~\ruleref{ST-Abs} and the
$\eta$-rules~\rulerefN{ST-Eta1}{ST-$\eta_{1,2}$}.  For example, for
the left-hand case and $K = \dfun{X}{K_1}{K_2}$ we have
\begin{alignat}{2}
\Gamma \; \ts \; B_1 \; &\tsub \; \lam{X}{K_1}{\app{B_1}{X}}
\tag{by~\rulerefN{ST-Eta2}{ST-$\eta_2$}}\\
&\tsub \; \lam{X}{K_1}{\app{A}{\,X}} \tag{by the IH and~\ruleref{ST-Abs}}\\
&\tsub \; A &\;\; \kin \; \dfun{X}{K_1}{K_2}.
\tag{by~\rulerefN{ST-Eta1}{ST-$\eta_1$}}
\end{alignat}
\end{proof}

Thanks to the admissible kinding and subtyping rules for higher-order
intervals and extrema, we can now easily derive judgments for forming,
introducing or eliminating bounded universal quantifiers over
arbitrary type operators.

For example, well-formedness of the
higher-order universal quantifier $\all{X \tsub A}{K}{B}$ can be
derived as
\begin{prooftree}
\AxiomC{$\Gamma \ts A \kin K$}
\LeftLabel{(kinding validity)}
\UnaryInfC{$\kindD{\Gamma}{K}$}
\LeftLabel{\rulerefP{K-TMin}}
\UnaryInfC{$\Gamma \ts \tmin{K} \kin \kmax{K}$}
\AxiomC{$\Gamma \ts A \kin K$}
\RightLabel{(\Cor{K-KMax})}
\UnaryInfC{$\Gamma \ts A \kin \kmax{K}$}
\LeftLabel{\rulerefP{Wf-HoIntv}}
\BinaryInfC{$\kindD{\Gamma}{\tmin{K} \hointv{\kmax{K}} A}$}
\LeftLabel{(\Lem{re-idx_kmax})}
\UnaryInfC{$\kindD{\Gamma}{\tmin{K} \hointv{K} A}$}
\AxiomC{$\typeD{\Gamma, X \kas \tmin{K} \hointv{K} A}{B}$}
\LeftLabel{\rulerefP{K-All}}
\BinaryInfC{$\typeD{\Gamma}{\all{X \tsub A}{K}{B}}$}
\end{prooftree}
The derivation uses the following lemma for simplifying interval
kinds; its proof is by structural induction on the index $K$.
\begin{lemma}\label{lem:re-idx_kmax}
Let $A$, $B$ be types and $K$ a kind. Then
$A \hointv{\kmax{K}} B \alEq A \hointv{K} B$
\end{lemma}

Similar derivations exist for the introduction and elimination rules.
\begin{corollary}[bounded quantification] The following rules for the
formation, introduction and elimination of bounded universal
quantifiers are admissible.
\end{corollary}
\begin{center}
\infruleSimp[K-AllBnd]
{\Gamma \ts A \kin K  \andalso
\typeD{\Gamma, X \kas \tmin{K} \hointv{K} A}{B}}
{\typeD{\Gamma}{\all{X \tsub A}{K}{B}}}

\infruleSimp[T-TAbsBnd]
{\Gamma \ts A \kin K  \andalso
\Gamma, X \kas \tmin{K} \hointv{K} A \ts t \tin B}
{\Gamma \ts \Lam{X \tsub A}{K}{t} \tin \all{X \tsub A}{K}{B}}

\infruleSimp[T-TAppBnd]
{\Gamma \ts t \tin \all{X \tsub A}{K}{B}  \andalso
\Gamma \ts C \tsub A \kin K}
{\Gamma \ts \app{t}{(\weakEtaExp{K}{C})} \tin
\subst{B}{X}{\weakEtaExp{K}{C}}}
\end{center}
Similar rules for the formation, abstraction and elimination of
bounded operators are also admissible.

Note that we need to $\eta$-expand the type argument $C$ in the
elimination rule~\ruleref{T-TAppBnd}
before it can by applied to $t$.  This is because $C$ has kind $K$,
while the polymorphic expression $t$ expects an argument of kind
$\tmin{K} \hointv{K} C$.  As discussed earlier, $C$ is not guaranteed
to inhabit that kind but its $\eta$-expansion is --
via~\ruleref{K-HoSing} and a subsequent widening of its kind from
$C \hointv{K} C$ to $\tmin{K} \hointv{K} C$.

There is an alternative encoding of higher-order bounded
quantification (and bounded type operators) that
separates the declaration of type variables from that of the subtyping
constraints imposed by their bounds, at the cost of using an auxiliary
type variable with potentially inconsistent bounds.  Assume a
partition of the set of type variable names into two distinct sets of
\emph{operator names} denoted by $\op{X}, \op{Y}, \dotsc$ and
\emph{constraint names} denoted by $\cst{X}, \cst{Y}, \dotsc$
We may then encode an upper-bounded type variable binding
$X \tsub A \kin K$ as a pair of bindings $\op{X} \kin K$,
$\cst{X} \kin \op{X} \hointv{K} A$, separating the declaration of the
operator name $X$ from the subtyping constraint $X \tsub A$.  For
example, the encoding of bounded universal quantifiers according to
this scheme would be
$\all{X \tsub A}{K}{B} = \all{\op{X}}{K}{\all{\cst{X}}{\op{X}
\hointv{K} A}{B}}$
where $\cst{X} \notin \fv(B)$.

The advantage of this encoding is a
cleaner separation between the uses of bounded variable bindings in
kinding and subtyping.  Whenever we want to refer to the original type
variable $X$ or its kind, we simply use $\op{X}$.  When we require a
proof of the fact that $X \tsub A$ we obtain one from $\cst{X}$
\rulerefN{ST-HoBnd1}{ST-HoBind$_2$}, and~\ruleref{ST-Trans}.  The same
is true when we instantiate type parameters.  For example, a type
application $\app{t}{C}$, where $t$ has type $\all{X \tsub A}{K}{B}$
and $C \tsub A$, is now desugared to
$\app{\app{t}{C}}{(\weakEtaExp{K}{C})}$, \ie only the second type
argument, which corresponds to the constraint parameter $\cst{X}$,
needs to be $\eta$-expanded, while the argument $C$ for the parameter
$\op{X}$ can be left as is.  Since $\cst{X}$ does not occur freely in
the codomain $B$ of the desugared universal type, the overall type of
the desugared application is just $\subst{B}{\op{X}}{C}$.
A clear drawback of this encoding is the necessary duplication of
bindings and the corresponding introduction and elimination forms
(abstraction, application).  In addition, the kind
$\op{X} \hointv{K} A$ of the constraint $\cst{X}$ has inconsistent
bounds in general, which can be problematic.

There is an obvious alternative definition for the family of kinds
$\kmax{K}$, namely $\kmax{K} = (\tmin{K}) \hointvP{K} (\tmax{K})$.
The original definition, given in~\Fig{encodings} of the paper
(page~\pageref{fig:encodings}), has the advantage of being independent
of the definition of the higher-order extrema $\tmax{K}$ and
This allowed us to prove properties such as~\ruleref{Wf-KMax}
and~\Lem{SK-KMax} admissible without appealing to any of the
properties of higher-order extrema, and thereby avoid some cyclic
dependencies in the proofs of the latter.  The alternative definition,
on the other hand, seems more intuitive.  To conclude the section, we
show that the two definitions are equal for well-formed kinds $K$.
\begin{lemma}\label{lem:kmax_hointv}
The kind $\kmax{K}$ is equal to the higher-order interval bounded by
$\tmin{K}$ and $\tmax{K}$.  If $\; \kindD{\Gamma}{K}$, then
$\Gamma \ts \kmax{K} \keq (\tmin{K}) \hointvP{K} (\tmax{K})$.
\end{lemma}
\begin{proof}[Proof of \Lem{kmax_hointv}]
By induction on the structure of $K$.  The base case is immediate.
In the inductive step, we use~\ruleref{SK-HoIntv} and the

Let $K = \dfun{X}{K_1}{K_2}$.  We want to show that
\[
\Gamma \; \ts \; \dfun{X}{K_1}{\kmax{K_2}} \; \keq \;
\dfun{Y}{K_1}{
(\app{\tmin{\dfun{X}{K_1}{K_2}}}{Y}) \hointvP{K_2}
\]
for some $Y$ that does not occur freely in
$\fv(\tmin{\dfun{X}{K_1}{K_2}})$ or
$\fv(\tmax{\dfun{X}{K_1}{K_2}})$.  By the IH, we have
$\Gamma \ts \kmax{K_2} \keq (\tmin{K_2}) \hointvP{K_2} (\tmax{K_2})$ but
we need to adjust the bounds of the right-hand interval.  We use the
following equation for the lower bound, and an similar one for the
upper bound.
\begin{align}
\Gamma \; \ts \; \app{\tmin{\dfun{X}{K_1}{K_2}}}{Y} \; &\alEq \;
\app{\lam{X}{K_1}{\tmin{K_2}}}{Y}
\tag{by definition}\\
&\teq \; \subst{\tmin{K_2}}{X}{Y}
\tag{by \ruleref{K-TMin} and \rulerefN{TEq-Beta}{TEq-$\beta$}}\\
&\alEq \; \tmin{K_2} \hspace{5em}\kin \; \kmax{K_2}. \tag{$\alpha$-renaming}
\end{align}
By~\ruleref{SK-Refl-KEq}, \ruleref{SK-HoIntv}
and~\ruleref{SK-AntiSym} we obtain
\[
\Gamma \; \ts \; (\tmin{K_2}) \hointvP{\kmax{K_2}} (\tmax{K_2})
\; \keq \;
(\app{\tmin{\dfun{X}{K_1}{K_2}}}{Y}) \hointvP{\kmax{K_2}}
\]
which we re-index using~\Lem{re-idx_kmax}.  We conclude
by~\ruleref{KEq-Refl} and~\ruleref{KEq-DArr}.
\end{proof}

\section{Simple Kinding of Normal Types}
\label{sec:simple}

This section introduces a system of \emph{simplified kinding}
judgments which provide a syntactic characterization of normal types
and allow us to establish important properties about hereditary
substitutions and normal forms, notably a pair of commutativity lemmas
(\Lem[Lemmas]{hsubst-comm} and~\ref{lem:weq-nf-hsubst}) that play an
important role in the development of \Sec{canonical} in the paper.

The contents of this section are based on Chapter~4 of the first
author's PhD~dissertation.  We refer the interested reader to the
dissertation for the full details~\cite[][Ch.~4]{Stucki17thesis}.

\subsection{Preliminaries}

Before we can introduce the simplified system, we need to introduce a
few auxiliary definitions and lemmas that were omitted from
\Sec{normalization} in the paper.

We start with the definition of \emph{shape contexts} -- the type of
context used in our simplified kinding judgments.
Shape contexts $\gamma$, $\delta$ are best thought of as typing
contexts consisting exclusively of type variable bindings~$X \kas k\;$
with shape annotations~$k$ (as opposed to full kind annotations~$K$).
Their grammar is defined as follows. \begin{align*}
\gamma, \delta &::= \cempty \orElse \gamma, X \kas k
\tag{Shape context}
\end{align*}
As for full contexts, we assume that the variables bound in a shape
context are all distinct.
We write $\dom(\gamma)$ for the set of variables bound in $\gamma$ and
$(\gamma, \delta)$ for the concatenation of two shape contexts with
disjoint domains.

\subsubsection{Weak Equality}
\label{sec:weak_eq}

Recall that \emph{weak equality} is an equivalence $A \wkEq B$ on
types and kinds that identifies operator abstractions up to the shape
of their domain annotations.
\begin{center}
\infruleSimpBase{(\ruledef{WEq-Abs})}
{\simpEq{J}{K}  \andalso  A \wkEq B}
{\lam{X}{J}{A} \wkEq \lam{X}{K}{B}}
\end{center}
Formally, weak equality is defined as the smallest congruence (\wrt to
all the type and kind formers) that includes both syntactic equality
and the above rule~\ruleref{WEq-Abs}.
It is easy to verify that weak equality is a congruence \wrt
ordinary substitution.
In the following sections, we will show that weak equality is also a
congruence \wrt hereditary substitution, $\eta$-expansion and
normalization, and that weakly equal kinds $K_1 \wkEq K_2$ have equal
shapes $\simpEq{K_1}{K_2}$.

\subsubsection{Properties of Hereditary Substitution}

Since it is defined pointwise on spines, hereditary substitution
commutes with spine concatenation.
\begin{lemma}\label{lem:hsubst-concat}
$\hsubst{(\scons{\vec{D}_1}{\vec{D}_2})}{X}{k}{E} \; \alEq \;
\end{lemma}
Just as for ordinary substitution, shapes are stable under hereditary
\begin{lemma}[stability of shapes under hereditary
$\ksimp{\hsubst{J}{X}{k}{A}} \alEq \ksimp{J}$.
\end{lemma}
\begin{proof}
By straightforward induction on the structure of $J$.
\end{proof}
As a consequence, weak equality is a congruence \wrt hereditary
substitution and reducing application.
\begin{lemma}\label{lem:weq-par-hsubst}
Weak equality is a congruence w.r.t.\ hereditary substitution and
reducing application.  Let $E_1 \wkEq E_2$,
\begin{enumerate}
\item\label{item:weq-hsubst-kind} if $K_1 \wkEq K_2$, then
$\hsubst{K_1}{X}{k}{E_1} \wkEq \hsubst{K_2}{X}{k}{E_2}$;
\item\label{item:weq-hsubst-elim} if $D_1 \wkEq D_2$, then
$\hsubst{D_1}{X}{k}{E_1} \wkEq \hsubst{D_2}{X}{k}{E_2}$;
\item\label{item:weq-hsubst-sp} if $\vec{D}_1 \wkEq \vec{D}_2$, then
$\hsubst{\vec{D}_1}{X}{k}{E_1} \wkEq
\hsubst{\vec{D}_2}{X}{k}{E_2}$;
\item\label{item:weq-rapp-elim} if $D_1 \wkEq D_2$, then
$\rapp{E_1}{k}{D_1} \wkEq \rapp{E_2}{k}{D_2}$;
\item\label{item:weq-rapp-sp} if $\vec{D}_1 \wkEq \vec{D}_2$, then
$\rapp{E_1}{k}{\vec{D}_1} \wkEq \rapp{E_2}{k}{\vec{D}_2}$.
\end{enumerate}
\end{lemma}
\begin{proof}
The structure of the proof mirrors that of the recursive definitions
of hereditary substitution and reducing application.  All five parts
are proven simultaneously, by induction on the structure of $k$.
Parts~\Item{weq-hsubst-kind}--\Item{weq-hsubst-sp} proceed by an
inner induction on the derivations of $K_1 \wkEq K_2$,
$D_1 \wkEq D_2$ and $\vec{D}_1 \wkEq \vec{D}_2$, respectively.
Parts~\Item{weq-rapp-elim} and~\Item{weq-rapp-sp} proceed by a case
analysis on the final rules used to derive $E_1 \wkEq E_2$ and
$\vec{D}_1 \wkEq \vec{D}_2$, respectively.  Part~\Item{weq-hsubst-elim} proceeds by a case analysis on the final
rule used to derive $F_1 \wkEq F_2$, where $F_1$ and $F_2$ are the
heads, respectively, of $E_1 = F_1 \vec{D}_1$ and
$E_2 = F_2 \vec{D}_2$.  In the case for~\ruleref{WEq-Abs}, we use
stability of kind simplification under hereditary substitution
In the variable case,
we use the IH twice: first for part~\Item{weq-hsubst-sp} to derive
$\hsubst{\vec{D}_1}{X}{k}{E_1} \wkEq \hsubst{\vec{D}_2}{X}{k}{E_2}$,
then for part~\Item{weq-rapp-sp}, to derive
$\rapp{E_1}{k}{(\hsubst{\vec{D}_1}{X}{k}{E_1})} \wkEq
\rapp{E_2}{k}{(\hsubst{\vec{D}_2}{X}{k}{E_2})}$.  In the second
instance, $k$ does not decrease nor is
$\hsubst{\vec{D}_1}{X}{k}{E_1} \wkEq \hsubst{\vec{D}_2}{X}{k}{E_2}$
a sub-derivation of the current premise.  This use of the IH
is nevertheless justified because any subsequent use of the IH for
part~\Item{weq-hsubst-elim} in the proof of part~\Item{weq-rapp-sp}
must occur after the use of the IH for part~\Item{weq-rapp-elim}, at
which point $k$ has necessarily decreased.
\end{proof}

\subsubsection{Properties of $\eta$-Expansion and Normalization}

Unsurprisingly, shapes are stable under normalization.
\begin{lemma}[stability of shapes under normalization]
\label{lem:simp-stable-nf}
$\ksimp{\nf{\Gamma}{K}} \alEq \ksimp{K}$.
\end{lemma}
\begin{proof}
By straightforward induction on the structure of $K$.
\end{proof}

Extending kind simplification pointwise to contexts, we define
$\ksimp{\Gamma}$ as
\begin{align*}
\ksimp{\cempty} &= \cempty &
\ksimp{\Gamma, x \tas A} &= \ksimp{\Gamma} &
\ksimp{\Gamma, X \kas K} &= \ksimp{\Gamma}, X \kas \ksimp{K}
\end{align*}
It is easy to see that context lookup commutes with simplification,
\ie $\ksimp{\Gamma}(X) = \ksimp{\Gamma(X)}$, and that simplified
contexts are stable under (hereditary) substitution and
normalization, \ie
\begin{align*}
\ksimp{\subst{\Gamma}{X}{A}} &= \ksimp{\Gamma} &
\ksimp{\hsubst{\Gamma}{X}{k}{A}} &= \ksimp{\Gamma} &
\ksimp{\nfCtx{\Gamma}} &= \ksimp{\Gamma}
\end{align*}

The following two lemmas show that $\eta$-expansion and normalization
preserve weak equality.  Importantly, this is true even if the
corresponding kinds and contexts, respectively, are not themselves
weakly equal but have equal shapes -- a much weaker requirement.

\begin{lemma}\label{lem:weq-etaexp}
Weak equality is preserved by $\eta$-expansion along kinds of equal
shape.  If $\simpEq{J}{K}$ and $D \wkEq E$, then
$\etaExp{J}{D} \wkEq \etaExp{K}{E}$.
\end{lemma}
\begin{proof}
By induction on the structure of $J$ and case analysis on the final
rule used to derive $D \wkEq E$.
\end{proof}

\begin{lemma}\label{lem:weq-nf}
Kinds and types normalize weakly equally in contexts that simplify
equally.  Let $\Gamma$ and $\Delta$ be contexts such that
$\simpEq{\Gamma}{\Delta}$.  Then
\begin{enumerate}
\item $\nf{\Gamma}{K} \wkEq \nf{\Delta}{K}$ for any kind $K$, and
\item $\nf{\Gamma}{A} \wkEq \nf{\Delta}{A}$ for any type $A$.
\end{enumerate}
\end{lemma}
\begin{proof}
Simultaneously, by induction on the structure of $K$ and $A$,
respectively.  In the type variable case $A = X$ we use
\Lem{weq-etaexp}; in the operator application case
$A = \app{A_1}{A_2}$ we use \Lem{weq-par-hsubst}.\Item{weq-hsubst-elim};
in the cases for dependent operator kinds, universal types and
operator abstraction, we use \Lem{weq-simpeq}.
\end{proof}

\subsection{The Simplified System}

The function $\nfRaw$ assigns to each raw type $A$ in a given context
$\Gamma$ a unique type $\nf{\Gamma}{A}$.  But as we have seen, the
type $\nf{\Gamma}{A}$ may not be $\beta\eta$-normal if $A$ is
ill-kinded.  In this section, we prove the converse: whenever $A$ is
well-kinded in $\Gamma$, the type $\nf{\nfCtx{\Gamma}}{A}$ is a
$\eta$-long $\beta$-normal form.  To do so, we first introduce a set
of \emph{simplified kinding} judgments.  Roughly, a simplified kinding
judgment $\gamma \ts E \kin k$ establishes that the type $E$ is a
normal form of \emph{shape} $k$ in the \emph{shape context} $\gamma$.
Given $\gamma \ts E \kin k$, we say that $E$ is a \emph{well-shaped}
or \emph{simply (well-)kinded normal form}, or just that $E$ is
\emph{simply kinded}.  As we are about to show, every well-kinded type
$\Gamma \ts A \kin K$ has a well-shaped normal form
$\ksimp{\Gamma} \ts E \kin \ksimp{K}$, namely
$E = \nf{\nfCtx{\Gamma}}{A}$ (see \Lem{nf-simp} below).

It is important to note that the converse is not true: not every
simply kinded type is well-kinded.  Because kind simplification
forgets dependencies, there are necessarily some ill-kinded types that
are considered simply well-kinded according to the judgments we are
about to introduce.  However, every simply kinded type is guaranteed
to be an $\eta$-long $\beta$-normal form and, as we will see in this
section, simple kinding is preserved by operations such as hereditary
substitution and $\eta$-expansion.  Hence simple kinding allows us to
prove important properties about these operations on
$\beta\eta$-normal forms without subjecting ourselves to the
complexity of fully dependent kinds.

To enhance readability, we use the following naming conventions for
normal forms: the metavariables $U$, $V$, $W$ denote normal types,
while $M$ and $N$ denote neutral types.\footnote{This is just
notation.  We do not consider normal forms a separate syntactic
category, \eg the letters $U$, $V$, $W$ are metavariables
denoting types (typically in elimination form) rather than
non-terminals in some grammar of normal forms.}  No special notation
is used for normal kinds.

\paragraph{Judgments.}  \Fig{simple_rules} defines the following
judgments by mutual induction.
\[\begin{array}{l@{\gap}l}
\kindS{\gamma}{K} &
\text{the kind $K$ is simply well-formed and normal in $\gamma$}\\
\gamma \ts V \kin k &
\text{the type $V$ is a normal form of shape $k$ in $\gamma$}\\
\gamma \tsNe N \kin k &
\text{the type $N$ is a neutral form of shape $k$ in $\gamma$}\\
\spS{\gamma}{j}{\vec{V}}{k} &
\text{applying an operator of shape $j$ to the normal spine
&\text{yields a type of shape $k$ in $\gamma$.}
\end{array}\]

\fig[tb]{fig:simple_rules}{Simplified kinding}{
\judgment{Simplified well-formedness of kinds}{\fbox{$\kindS{\gamma}{K}$}}
\begin{center}
\begin{minipage}[t]{0.44\linewidth}
\infruleLeft{SWf-Intv}
{\typeS{\gamma}{U} \andalso \typeS{\gamma}{V}}
{\kindS{\gamma}{U \intv V}}
\end{minipage}\hspace{1ex}
\begin{minipage}[t]{0.54\linewidth}
\infruleLeft{SWf-DArr}
{\kindS{\gamma}{J} \andalso \kindS{\gamma, X \kas \ksimp{J}}{K}}
\end{minipage}
\end{center}

\judgment{Kinding of neutral types}{\fbox{$\gamma \tsNe N \kin k$}}

\infruleLeft{SK-VarApp}
{\gamma(X) = j  \andalso  \gamma \ts j \kin \vec{V} \kin k}
{\gamma \tsNe \app{X}{\vec{V}} \kin k}

\judgment{Simple spine kinding}{\fbox{$\spS{\gamma}{j}{\vec{V}}{k}$}}
\begin{center}
\begin{minipage}[t]{0.42\linewidth}
\infruleLeft{SK-Empty}{\quad}{\spS{\gamma}{k}{\sempty}{k}}
\end{minipage}\hspace{1ex}
\begin{minipage}[t]{0.56\linewidth}
\infruleLeft{SK-Cons}
{\gamma \ts U \kin j \andalso \spS{\gamma}{k}{\vec{V}}{l}}
{\spS{\gamma}{\fun{j}{k}}{\scons{U}{\vec V}}{l}}
\end{minipage}
\end{center}\medskip

\judgment{Simple kinding of normal types}{\fbox{$\gamma \ts V \kin k$}}
\begin{multicols}{2}
\typicallabel{SK-Sing}
\infrule[\ruledef{SK-Top}]

\infrule[\ruledef{SK-Arr}]
{\typeS{\gamma}{U}  \andalso  \typeS{\gamma}{V}}

\infrule[\ruledef{SK-Abs}]
{\kindS{\gamma}{J}  \andalso  \gamma, X \kas \ksimp{J} \ts V \kin k}
{\gamma \ts \lam{X}{J}{V} \kin \fun{\ksimp{J}}{k}}

\infrule[\ruledef{SK-Bot}]

\infrule[\ruledef{SK-All}]
{\kindS{\gamma}{K}  \andalso  \typeS{\gamma, X \kas \ksimp{K}}{V}}

\infrule[\ruledef{SK-Ne}]
{\gamma \tsNe N \kin \kstar}
\end{multicols}}

The judgments for simple kind formation and kinding follow the
syntactic structure of normal kinds and types.  A type $V$ is a
$\beta\eta$-normal form $\gamma \ts V \kin k$ of shape $k$ if it
is either a proper type introduced by one of the basic type formers
applied to normal arguments (rules~\ruleref{SK-Top}, \ruleref{SK-Bot},
\ruleref{SK-Arr}, and~\ruleref{SK-All}), an operator abstraction with
a normal body (rule~\ruleref{SK-Abs}), or a simply kinded
neutral type (rule~\ruleref{SK-Ne}).  Simply kinded neutral forms
$\gamma \tsNe N \kin k$ are eliminations headed by an abstract type
operator, \ie a type variable $X$, which is applied to a spine of
normal types $\vec{V}$ (rule~\ruleref{SK-VarApp}).  Finally, a simply
well-formed normal kind $\kindS{\gamma}{K}$ is either a type interval
bounded by normal types (rule~\ruleref{SWf-Intv}) or a dependent arrow
with normal domain and codomain (rule~\ruleref{SWf-DArr}).  Note that
type operator abstractions are the only normal forms of arrow shape.
This ensures that normal types are always $\eta$-long.

The simple spine kinding judgment $\spS{\gamma}{j}{\vec{V}}{k}$ is
different from the other judgment forms in that it is a quaternary
rather than a ternary relation.  The shapes $j$ and $k$ should be read
as inputs and outputs, respectively, of such judgments: when a type of
shape $j$ is applied to the spine $\vec{V}$ (the subject of the judgment), the resulting type
is of shape $k$ -- as exemplified by the rule~\ruleref{SK-VarApp}.

There is no formation judgment for shape contexts $\gamma$ since such
contexts only contain bindings assigning shapes to type variables, and there is no such
thing as an ill-formed simple kind.

Because kinding is simplified, there is no notion of subkinding or
kind equality, and hence no need for a subsumption rule.  As a
consequence, the simple kind formation and kinding rules are
Another important property of simplified kinding is that none of the
rules involve substitutions in kinds.
This substantially simplifies the proofs of key lemmas about
hereditary substitutions, in particular that of \Lem{simp-hsubst}
which states that hereditary substitutions preserve simple kinding
(and thus normal forms).
It is also important in establishing admissibility of the following
simple rules about spines and neutral types.

\begin{lemma}
The following simple kinding rules for spine concatenation and
application of neutrals are admissible.
\end{lemma}
\begin{center}
\infruleSimp[SK-Concat]
{\spS{\gamma}{j}{\vec{U}}{k}  \andalso  \spS{\gamma}{k}{\vec{V}}{l}}
{\spS{\gamma}{j}{\scons{\vec U}{\vec V}}{l}}
\hspace{2em}
\infruleSimp[SK-Snoc]
{\spS{\gamma}{j}{\vec{U}}{\fun{k}{l}}  \andalso  \gamma \ts V \kin k}
{\spS{\gamma}{j}{\scons{\vec U}{V}}{l}}
\hspace{2em}
\infruleSimp[SK-NeApp]
{\gamma \tsNe N \kin \fun{j}{k}  \andalso  \gamma \ts V \kin j}
{\gamma \tsNe \app{N}{V} \kin k}
\end{center}
\begin{proof}
The proofs are done separately for each of the three rules in the
order the rules are listed.  The proof for~\ruleref{SK-Concat} is by
induction on the derivation of the first premise. The
rule~\ruleref{SK-Cons} is derivable from~\ruleref{SK-Snoc} as a
special case where $\vec{V} = \scons{V}{\sempty}$,
using~\ruleref{SK-Empty} and~\ruleref{SK-Cons}.  The proof
of~\ruleref{SK-NeApp} starts with a case analysis on the final rule
used to derive $\Gamma \tsNe N \kin \fun{j}{k}$.  The only rule for
deriving such judgments is~\ruleref{SK-VarApp}, hence $N$ must be of
the form $N = \app{X}{\vec{U}}$ with $\gamma(X) = l$ and
$\gamma \ts l \kin \vec{U} \kin \fun{j}{k}$.  We conclude
by~\ruleref{SK-Snoc} and~\ruleref{SK-VarApp}.
\end{proof}

\subsubsection{Simply-Kinded Hereditary Substitution}
\label{sec:simple_hsubst}

Before we can prove that hereditary substitutions preserve simple
kinding, we first need to establish the usual weakening properties for
simple kind formation and kinding.

\begin{lemma}[weakening]\label{lem:simp-weaken}
A simple judgment remains true if its context is extended by an
additional binding.  Let $\gamma$, $\delta$ be shape contexts, $k$ a
shape and $X \notin \dom(\gamma, \delta)$.  If
$\; \judgS{\gamma, \delta}$ for any of the simple judgments defined
above, then $\judgS{\gamma, X \kas k, \delta}$.
\end{lemma}
\begin{proof}
Simultaneously for all four judgments, by induction on the
derivation of $\; \judgS{\gamma, \delta}$.
\end{proof}
\begin{corollary}[Iterated weakening]\label{cor:simp-iter-weaken}
Given a pair $\gamma$, $\delta$ of disjoint shape contexts, if
$\; \judgS{\gamma}$, then $\judgS{\gamma, \delta}$.
\end{corollary}

\begin{lemma}[hereditary substitution]\label{lem:simp-hsubst}
Hereditary substitutions and reducing applications preserve the
shapes of types and simple well-formedness of kinds.  Let $\gamma$,
$\delta$ be shape contexts and $X$ such that
$X \notin \dom(\gamma, \delta)$.  Assume further that
$\gamma \ts V \kin k$ for some $V$ and $k$.  Then
\begin{enumerate}
\item\label{item:simp-hsubst-kds} if
$\; \kindS{\gamma, X \kas k, \delta}{J}$, then
$\kindS{\gamma, \delta}{\hsubst{J}{X}{k}{V}}$;
\item\label{item:simp-hsubst-nf} if
$\; \gamma, X \kas k, \delta \ts U \kin j$, then
$\gamma, \delta \ts \hsubst{U}{X}{k}{V} \kin j$;
\item\label{item:simp-hsubst-ne} if
$\; \gamma, X \kas k, \delta \tsNe N \kin j$, then
$\gamma, \delta \ts \hsubst{N}{X}{k}{V} \kin j$ as a normal form;
\item\label{item:simp-hsubst-sp} if
$\; \spS{\gamma, X \kas k, \delta}{j}{\vec{U}}{l}$, then
$\spS{\gamma, \delta}{j}{\hsubst{\vec{U}}{X}{k}{V}}{l}$;
\item\label{item:simp-rapp-nf} if $k = \fun{k_1}{k_2}$ and
$\; \gamma \ts U \kin k_1$, then
$\gamma \ts \rapp{V}{\fun{k_1}{k_2}}{U} \kin k_2$;
\item\label{item:simp-rapp-sp} if
$\; \spS{\gamma}{k}{\vec{U}}{j}$, then
$\gamma \ts \rapp{V}{k}{\vec{U}} \kin j$.
\end{enumerate}
\end{lemma}
Note that hereditary substitutions preserve the shapes of neutral
types but not neutrality itself.
\begin{proof}
All six parts are proven simultaneously by induction on the
structure of $k$.
Parts~\Item{simp-hsubst-kds}--\Item{simp-hsubst-sp} proceed by an
inner induction on the simple formation or kinding derivations for
$J$, $U$, $N$ and $\vec{U}$, respectively.
Parts~\Item{simp-rapp-nf} and~\Item{simp-rapp-sp} proceed by a case
analysis on the final rules used to derive
$\gamma \ts V \kin \fun{k_1}{k_2}$ and
$\spS{\gamma}{k}{\vec{V}}{j}$, respectively; for
part~\Item{simp-rapp-nf}, the only applicable rule
is~\ruleref{SK-Abs}.  For part~\Item{simp-hsubst-ne}, in the case
for~\ruleref{SK-VarApp} when $N = \app{X}{\vec{U}}$, we use iterated
weakening (\Cor{simp-iter-weaken}) and the IH
(for~\Item{simp-hsubst-sp}), respectively, to obtain
$\gamma, \delta \ts V \kin k$ and
$\spS{\gamma, \delta}{k}{\hsubst{\vec{U}}{X}{k}{V}}{j}$.  To
conclude the case, we apply the IH again (for~\Item{simp-rapp-sp}).
In this second use of the IH, $k$ does not decrease nor is
$\spS{\gamma, \delta}{k}{\hsubst{\vec{U}}{X}{k}{V}}{j}$ a strict
sub-derivation of the current premise.  However, in order to use the
IH for part~\Item{simp-hsubst-ne} again from within the proof of
part~\Item{simp-rapp-sp}, we must go through
part~\Item{simp-rapp-nf}, at which point $k$ necessarily decreases.
Again, the structure of the proof mirrors that of the mutually
recursive definitions of hereditary substitution and reducing
\end{proof}

Thanks to \Lem{simp-hsubst}, we can now prove the following
commutativity lemma about hereditary substitutions, which will play an
important role in the proof of \Lem{weq-nf-hsubst} below and in
\Sec{canonical} of the paper.

\begin{lemma}[commutativity of hereditary
Hereditary substitutions of simply kinded types commute; hereditary
substitutions of simply kinded types commute with simply kinded
reducing applications.  Let $\gamma_1 \ts U \kin j$ and
$\gamma_1, X \kas j, \gamma_2 \ts V \kin k$.  Then
\begin{enumerate}[nosep]
\item\label{item:hsubst-comm-kds} if
$\; \kindS{\gamma_1, X \kas j, \gamma_2, Y \kas k, \gamma_3}{J}$, then
\[
\hsubst{\hsubst{J}{Y}{k}{V}}{X}{j}{U} \; \alEq \;
\hsubst{\hsubst{J}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}};
\]
\item\label{item:hsubst-comm-nf} if
$\; \gamma_1, X \kas j, \gamma_2, Y \kas k, \gamma_3 \ts W \kin l$, then
\[
\hsubst{\hsubst{W}{Y}{k}{V}}{X}{j}{U} \; \alEq \;
\hsubst{\hsubst{W}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}};
\]
\item\label{item:hsubst-comm-ne} if
$\; \gamma_1, X \kas j, \gamma_2, Y \kas k, \gamma_3 \tsNe N \kin l$, then
\[
\hsubst{\hsubst{N}{Y}{k}{V}}{X}{j}{U} \; \alEq \;
\hsubst{\hsubst{N}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}};
\]
\item\label{item:hsubst-comm-sp} if
$\; \spS{\gamma_1, X \kas j, \gamma_2, Y \kas k,
\gamma_3}{l_1}{\vec{W}}{l_2}$,
\[
\hsubst{\hsubst{\vec{W}}{Y}{k}{V}}{X}{j}{U} \; \alEq \;
\hsubst{\hsubst{\vec{W}}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}};
\]
\item\label{item:rapp-comm-nf} if $k = \fun{k_1}{k_2}$ and
$\; \gamma_1, X \kas j, \gamma_2 \ts W \kin k_1$, then
\[
\hsubst{(\rapp{V}{\fun{k_1}{k_2}}{W})}{X}{j}{U} \; \alEq \;
\rapp{(\hsubst{V}{X}{j}{U})}{\fun{k_1}{k_2}}{(\hsubst{W}{X}{j}{U})};
\]
\item\label{item:rapp-comm-sp} if
$\; \spS{\gamma_1, X \kas j, \gamma_2}{k}{\vec{W}}{l}$, then
$\hsubst{(\rapp{V}{k}{\vec{W}})}{X}{j}{U} \; \alEq \;
\rapp{(\hsubst{V}{X}{j}{U})}{k}{(\hsubst{\vec{W}}{X}{j}{U})}$.
\end{enumerate}
\end{lemma}
\begin{proof}All six parts are proven simultaneously by simultaneous induction on
the structures of $j$ and $k$.  Simultaneous structural induction on
$j$ and $k$ means roughly that it is sufficient for either one of
$j$ or $k$ to decrease in an induction step.  More formally, denote
by $\sqsubseteq$ the sub-expression order on shapes, then the
simultaneous induction order $<$ on unordered pairs $\set{ j, k }$
of shapes is defined as $\set{ j_1, j_2 } < \set{ k_1, k_2 }$ if
$j_1 \sqsubset k_1$ and $j_2 \sqsubseteq k_2$.
Importantly, $<$ is defined over \emph{unordered} pairs which allows
us to exchange $j$ and $k$ in an induction step.
proceed by an inner induction on the simple formation or kinding
derivations for $J$, $W$, $N$ and $\vec{W}$, respectively.

As usual, the interesting cases are those for
part~\Item{hsubst-comm-ne}, when $N = \app{Y}{\vec{W}}$ and
$N = \app{X}{\vec{W}}$.
\begin{itemize}
\item \emph{Case \ruleref{SK-VarApp}, $N = \app{Y}{\vec{W}}$.}  We
$\spS{\gamma_1, X \kas j, \gamma_2, Y \kas k,
\gamma_3}{k}{\vec{W}}{l}$.
By \Lem{simp-hsubst}.\Item{simp-hsubst-sp}, we obtain
$\spS{\gamma_1, X \kas j, \gamma_2,
\gamma_3}{k}{\hsubst{\vec{W}}{Y}{k}{V}}{l}$, and hence we have
\begin{align*}\hspace{-2em}
\hsubst{\hsubst{(\app{Y}{\vec{W}})&}{Y}{k}{V}}{X}{j}{U}\\
&\alEq \;
\hsubst{(\rapp{V}{k}{(\hsubst{\vec{W}}{Y}{k}{V})})}{X}{j}{U}
\tag{by definition}\\
&\alEq \;
\rapp{(\hsubst{V}{X}{j}{U})}{k}{(
\hsubst{\hsubst{\vec{W}}{Y}{k}{V}}{X}{j}{U})}
\tag{by the IH for~\Item{rapp-comm-sp}}\\
&\alEq \;
\rapp{(\hsubst{V}{X}{j}{U})}{k}{(
\hsubst{\hsubst{\vec{W}}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}})}
\tag{by the IH for~\Item{hsubst-comm-sp}}\\
&\alEq \;
\hsubst{\hsubst{(\app{Y}{\vec{W}})}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}}.
\tag{by definition}
\end{align*}
\item \emph{Case \ruleref{SK-VarApp}, $N = \app{X}{\vec{W}}$.}  We
$\spS{\gamma_1, X \kas j, \gamma_2, Y \kas k,
\gamma_3}{j}{\vec{W}}{l}$.
By \Lem{simp-hsubst}.\Item{simp-hsubst-sp}, we obtain
$\spS{\gamma_1, X \kas j, \gamma_2,
\gamma_3}{j}{\hsubst{\vec{W}}{Y}{k}{V}}{l}$, and hence we have
\begin{align*}\hspace{-2em}
\hsubst{\hsubst{(\app{X}{\vec{W}})&}{Y}{k}{V}}{X}{j}{U}\\
&\alEq \;
\hsubst{(\app{X}{(\hsubst{\vec{W}}{Y}{k}{V})})}{X}{j}{U}
\tag{by definition}\\
&\alEq \;
\rapp{U}{j}{(
\hsubst{\hsubst{\vec{W}}{Y}{k}{V}}{X}{j}{U})}
\tag{by definition}\\
&\alEq \;
\rapp{U}{j}{(
\hsubst{\hsubst{\vec{W}}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}})}
\tag{by the IH for~\Item{hsubst-comm-sp}}\\
&\alEq \;
\rapp{(\hsubst{U}{Y}{k}{\hsubst{V}{X}{j}{U}})}{j}{(
\hsubst{\hsubst{\vec{W}}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}})}
\tag{as $Y \notin \fv(U)$}\\
&\alEq \;
\hsubst{(\rapp{U}{j}{(
\hsubst{\vec{W}}{X}{j}{U})})}{Y}{k}{\hsubst{V}{X}{j}{U}}
\tag{by the IH for~\Item{rapp-comm-sp}}\\
&\alEq \;
\hsubst{\hsubst{(\app{X}{\vec{W}})}{X}{j}{U}}{Y}{k}{\hsubst{V}{X}{j}{U}}.
\tag{by definition}
\end{align*}
\end{itemize}
Note that, in the second case, we switched the roles of the shape
$j$ and $k$ when invoking the IH for part~\Item{rapp-comm-sp}.
\end{proof}

\subsubsection{Simplification and Normalization of Kinding}
\label{sec:simple_nf}

Thanks to \Lem{nf-sound} we know that the definition of the
normalization function $\nfRaw$ is sound, \ie that well-formed kinds
$\kindD{\Gamma}{K}$ and well-kinded types $\Gamma \ts A \kin K$ are
convertible with $\nf{\nfCtx{\Gamma}}{K}$ and
$\nf{\nfCtx{\Gamma}}{A}$, respectively.  But we have yet to establish
that $\nf{\nfCtx{\Gamma}}{K}$ and $\nf{\nfCtx{\Gamma}}{A}$ are
actually normal forms.  In this section, we prove a more general
result, namely that, whenever $\kindD{\Gamma}{K}$ and
$\Gamma \ts A \kin K$,
it follows that $\nf{\nfCtx{\Gamma}}{K}$ is a simply well-formed
normal kind and and $\nf{\nfCtx{\Gamma}}{A}$ is a simply well-kinded
normal type.

As a first step, we show that the shapes of variables and, more
generally, of neutral types are preserved by $\eta$-expansion.
\begin{lemma}\label{lem:sk-etaexp}
$\eta$-expansion preserves the shapes of neutral types.
Assume $\kindS{\gamma}{K}$ and $\gamma \tsNe N \kin \ksimp{K}$.
Then $\gamma \ts \etaExp{K}{N} \kin \ksimp{K}$.
\end{lemma}
\begin{proof}
By induction on the structure of $K$.  The case fore
$K = \dfun{X}{K_1}{K_2}$ proceeds by case analysis on the final
rules used to derive $\kindS{\gamma}{\dfun{X}{K_1}{K_2}}$ and
$\gamma \tsNe N \kin \fun{\ksimp{K_1}}{\ksimp{K_2}}$ and uses the
weakening lemma (\Lem{simp-weaken}) as well as~\ruleref{SK-NeApp}.
\end{proof}

Next, we require a syntactic notion of normal contexts.  We define the
\emph{simple context formation} judgment $\ctxS{\Gamma}$ as the
pointwise lifting of simple kind formation and kinding to bindings:
\begin{center}
\infruleSimp {\quad}{\ctxS{\cempty}}
\hspace{3em}
\infruleSimp {\ctxS{\Gamma}  \andalso  \kindS{\ksimp{\Gamma}}{K}}
{\ctxS{\Gamma, X \kas K}}
\hspace{3em}
\infruleSimp {\ctxS{\Gamma}  \andalso  \ksimp{\Gamma} \ts V \kin \kstar}
{\ctxS{\Gamma, x \kas V}}
\end{center}

Since simple kind formation and kinding is defined on normal kinds and
types, a simply well-formed context $\Gamma$ is also normal.
Conversely, if we lookup the declared kind or type of a variable in a
simply well-formed context, the result is guaranteed to be a normal

\begin{lemma}\label{lem:sc-lookup}
The declared kinds and types of variables in a simply well-formed
context $\Gamma$ are simply well-formed and well-kinded,
respectively, in $\ksimp{\Gamma}$, i.e
\end{lemma}
\begin{center}
\infruleSimp[SC-TpLookup]
{\ctxS{\Gamma, X \kas K, \Delta}}
{\kindS{\ksimp{\Gamma, X \kas K, \Delta}}{K}}
\hspace{3em}
\infruleSimp[SC-TmLookup]
{\ctxS{\Gamma, x \tas V, \Delta}}
{\typeS{\ksimp{\Gamma, x \tas V, \Delta}}{V}}
\end{center}
\begin{proof}
Both parts are proven separately by structural induction on $\Delta$
and case analysis on the final rule used to derive the premise.  In
the inductive case, we use the weakening lemma for simple kind
\end{proof}

With \Lem[Lemmas]{sk-etaexp} and~\ref{lem:sc-lookup} at hand, it is
easy to show that $\nfRaw$ does indeed produce normal forms.
\begin{lemma}[normalization and simplification]\label{lem:nf-simp}
Well-formed kinds and well-kinded types have simply well-formed and
simply kinded normal forms, respectively.
\begin{enumerate}
\item\label{item:nf-simp-kd} If $\; \kindD{\Gamma}{K}$, then
\item\label{item:nf-simp-tp} If $\; \Gamma \ts A \kin K$, then
$\ksimp{\nfCtx{\Gamma}} \ts \nf{\nfCtx{\Gamma}}{A} \kin \ksimp{K}$.
\item\label{item:nf-simp-ctx} If $\; \ctxD{\Gamma}$, then
\end{enumerate}
\end{lemma}
The proof uses the following helper lemma about the shapes of
subkinds, which is proven by straightforward induction on subkinding
\begin{lemma}\label{lem:simp-decl-sk}
Subkinds have equal shapes.  If $\; \Gamma \ts J \ksub K$, then
$\ksimp{J} \alEq \ksimp{K}$.
\end{lemma}

\begin{proof}[Proof of \Lem{nf-simp}]
Simultaneously by induction on declarative kind formation, kinding,
and context formation derivations.  The only interesting cases
are~\ruleref{K-Sub} (where we use \Lem{simp-decl-sk}),
\ruleref{K-Var} and \ruleref{K-App}.  In the case for
\ruleref{K-Var}, where $A = X$, we use the IH for
part~\Item{nf-simp-ctx} and \ruleref{SC-TpLookup} to obtain
$\kindS{\ksimp{\nfCtx{\Gamma}}}{K}$ for $K = \nfCtx{\Gamma}(X)$, and
we conclude by \Lem{sk-etaexp}.  In the case for~\ruleref{K-App},
where $A = \app{A_1}{A_2}$, we start by applying the IH to obtain
$\ksimp{\nfCtx{\Gamma}} \ts \nf{\nfCtx{\Gamma}}{A_1} \kin
\fun{\ksimp{K_1}}{\ksimp{K_2}}$, and
$\ksimp{\nfCtx{\Gamma}} \ts \nf{\nfCtx{\Gamma}}{A_2} \kin
\ksimp{K_1}$.
The first of these judgments must be derived using~\ruleref{SK-Abs}
because that is the only simple kinding rule assigning an arrow kind
to a type.  Hence $\nf{\nfCtx{\Gamma}}{A_1} = \lam{X}{J}{V}$ for
some $J$ and $V$ such that $\simpEq{J}{K_1}$ and
$\ksimp{\nfCtx{\Gamma}}, X \kas \ksimp{K_1} \ts V \kin \ksimp{K_2}$.
We conclude by the hereditary substitution lemma for normal types
(\Lem{simp-hsubst}.\Item{simp-hsubst-nf}) and
\Lem{simp-stable-hsubst}.
\end{proof}

\subsubsection{Commutativity of Normalization and Substitution}
\label{sec:comm-nf-subst}

Our final task in this section is to establish another commutativity
property that will play a crucial role in proving equality of
declarative and canonical subtyping: the fact that normalization
commutes with substitution.

In the past few sections, we have seen that well-formed kinds and
well-kinded types have normal forms (\Lem{nf-simp}) and that these
normal forms are convertible to the kinds and types they were computed
from (\Lem{nf-sound}).  By validity, context conversion and kind
conversion, this means that every declarative subtyping judgment
$\Gamma \ts A \tsub B \kin K$ has an associated judgment
$\nfCtx{\Gamma} \ts \nf{}{A} \tsub \nf{}{B} \kin \nf{}{K}$ relating
the normal forms of the original expressions.

In \Sec{canonical} of the paper, we describe a system of canonical
rules for deriving such judgments which are defined directly on normal
forms -- similar to the simple kinding and kind formation judgments
introduced in this section.
The proof of equivalence of the two systems requires one canonical
--~possibly a derivable or admissible one~--
for every declarative rule.
But some of the declarative rules, such as the subtyping
rules~\rulerefN{ST-Beta1}{ST-$\beta_{1,2}$} for $\beta$-conversions,
or the kinding rule~\ruleref{K-App} for applications, involve
substitutions, which do not preserve normal forms.
To see why this is
a problem, consider the declarative rule~\ruleref{K-App}:
\begin{center}
\infruleSimp
{\Gamma \ts A \kin \dfun{X}{J}{K}  \andalso  \Gamma \ts B \kin J}
{\Gamma \ts \app{A}{B} \kin \subst{K}{X}{B}}
\end{center}
By soundness of normalization (\Lem{nf-sound}), type equation validity
(\Lem{decl_validity}), and context conversion (\Cor{decl_ctx_conv}),
we know that the following is also admissible:
\begin{center}
\infruleSimp
{\nfCtx{\Gamma} \ts U \kin \dfun{X}{J'}{K'}  \andalso
\nfCtx{\Gamma} \ts V \kin J'}
{\nfCtx{\Gamma} \ts \nf{}{\app{A}{B}} \kin \nf{}{\subst{K}{X}{B}}}
\end{center}
where $U = \nf{}{A}$, $V = \nf{}{B}$,
$J' = \nf{}{J}$ and $K' = \nf{}{K}$.  By \Lem{nf-simp}, we know that
$U$ and $V$ are simply well-kinded normal types, and that $J'$ and
$K'$ are simply well-formed normal kinds.  For our canonical
application rule, we would like to express the type
$\nf{}{\app{A}{B}}$ and the kind $\nf{}{\subst{K}{X}{B}}$ in the
conclusion directly using $U$, $V$, $J'$ and $K'$.  This is relatively
straightforward for the application $\nf{}{\app{A}{B}}$ because we
know that $U$ must be an operator abstraction $U = \lam{X}{L}{W}$;
after all, $U$ has shape $\fun{\ksimp{J}}{\ksimp{K}}$ and normal
forms are $\eta$-long.  We also know that
$\ksimp{L} \alEq \ksimp{J} \alEq \ksimp{J'}$ (see the proof of
\Lem{nf-simp} for details).  Hence
$\nf{}{\app{A}{B}} \alEq \hsubst{W}{X}{\ksimp{J'}}{V}$ by definition
of $\nfRaw$, and we are done.

Things are more complicated for the normal kind
$\nf{}{\subst{K}{X}{B}}$.  The definition of the normalization
function $\nfRaw$ does not tell us anything immediately useful about
substitutions.  Indeed, we know that substitutions do not preserve
normal forms, \eg $\subst{(\app{Y}{V})}{Y}{\lam{X}{J'}{W}}$ is not a
normal form, even if $\app{Y}{V}$ and $\lam{X}{J'}{W}$ are.  However,
\Cor{hsubst-sound}.\Item{hsubst-snd-kind} tells us that substitutions
in kinds are judgmentally equal to hereditary substitutions, \ie
$\Gamma \ts \subst{K}{X}{B} \keq \hsubst{K}{X}{\ksimp{J'}}{B}$, and
\Lem{simp-hsubst}.\Item{simp-hsubst-kds} tells us that hereditary
substitutions preserve normal forms, all of which suggests that
$\nf{}{\subst{K}{X}{B}}$ should be equal to
$\hsubst{K'}{X}{\ksimp{J'}}{V}$.  This is indeed the case; one can
show that
$\Gamma \ts \nf{}{\subst{K}{X}{B}} \keq
\hsubst{K'}{X}{\ksimp{J'}}{V}$.
But there is a caveat: the two normal forms are not
\emph{syntactically} equal, \ie
$\nf{}{\subst{K}{X}{B}} \, \not\alEq \, \hsubst{K'}{X}{\ksimp{J'}}{V}$.
$\nf{}{\subst{A}{X}{B}} \, \not\alEq \, \hsubst{\nf{}{A}}{X}{k}{\nf{}{B}}$
for types $A$ and $B$ in general.

This fact is best illustrated through the case of type variables,
\ie when $A = X$ and we have
$\nf{\Gamma}{\subst{X}{X}{B}} \alEq \nf{\Gamma}{B}$ and
$\hsubst{(\nf{\Gamma}{X})}{X}{k}{\nf{}{B}} \alEq
\hsubst{(\etaExp{\Gamma(X)}{X})}{X}{k}{\nf{}{B}}$.
We would like to show that $\hsubst{(\etaExp{K}{X})}{X}{k}{V}$ is
syntactically equal to $V$ at least when all the involved types and
kinds are well-kinded and well-formed, \ie when
$\Gamma \ts X \kin K$, $\; \Gamma \ts V \kin K$ and $k = \ksimp{K}$.
But this is not the case.  The culprit is a mismatch of kind
annotations in operator abstractions, as illustrated by the following

Let $J_1 = \Top \intv \Top$ and $J_2 = \kstar$ so that
$\Gamma \ts J_1 \ksub J_2$ for any context $\Gamma$.  Let $U = \Top$,
$V = \lam{X}{J_2}{U}$ and $K = \dfun{X}{J_1}{\kstar}$ so that
$\Gamma \ts V \kin \dfun{X}{J_2}{\kstar}$,
$\Gamma \ts \dfun{X}{J_2}{\kstar} \ksub K$ and hence
$\Gamma \ts V \kin K$. Then
\begin{alignat*}{2}
\etaExp{K}{Y} &&& \; \alEq \; \lam{Z}{J_1}{\app{Y}{Z}}\\
\hsubst{\etaExp{K}{Y}&}{Y}{\ksimp{K}}{V} && \; \alEq \;
\hsubst{(\lam{Z}{J_1}{\app{Y}{Z}})}{Y}{\ksimp{K}}{V} \\
&&& \; \alEq \; \lam{Z}{J_1}{\hsubst{(\app{Y}{Z})}{Y}{\ksimp{K}}{V}}
\tag{because $Y \notin \fv(J_1)$}\\
&&& \; \alEq \; \lam{Z}{J_1}{\rapp{V}{\ksimp{K}}{Z}} \\
&&& \; \alEq \;
\lam{Z}{J_1}{\rapp{\lam{X}{J_2}{U}}{\fun{\ksimp{J_1}}{\kstar}}{Z}} \\
&&& \; \alEq \; \lam{Z}{J_1}{\hsubst{U}{X}{\ksimp{J_1}}{Z}} \\
&&& \; \alEq \; \lam{X}{J_1}{U}  \tag{as $X, Z \notin \fv(U)$} \\
&&& \; \not\alEq \; \lam{X}{J_2}{U} \; \alEq \; V.
\tag{because $J_1 \not\alEq J_2$}
\end{alignat*}
So we are forced to conclude that
$\hsubst{\etaExp{K}{Y}}{Y}{\ksimp{K}}{V} \not\alEq V$ in general.  The
problem, as illustrated by this example, is that the domain annotation
$J_2$ of the type operator abstraction $V = \lam{X}{J_2}{U}$ is not
necessarily preserved by the hereditary substitution.  It is replaced
by the domain $J_1$ of the declared kind $K = \dfun{X}{J_1}{U}$ of
$Y$, which need not be \emph{syntactically} equal to $J_1$.

However, we do have $\Gamma \ts J_1 \ksub J_2$ and thus
$\simpEq{J_1}{J_2}$.  The solution, therefore, is to be more lenient
when comparing domain annotations in operator abstractions: the
\emph{weak} equation $\hsubst{\etaExp{K}{Y}}{Y}{\ksimp{K}}{V} \wkEq V$
does hold.  In fact, it holds for any simply well-formed kind $K$ and
simply well-kinded type $U$, as the following lemma shows.

\begin{lemma}\label{lem:etaexp-hsubst}
\begin{enumerate}[nosep]
\item\label{item:etaexp-ne-hsubst} Let
$\; \kindS{\gamma, X \kas j, \delta}{K}$, $\; \gamma \ts U \kin j$
$\; \gamma, X \kas j, \delta \tsNe \app{X}{\vec{V}} \kin
\ksimp{K}$.
\[
\hsubst{(\etaExp{K}{\app{X}{\vec{V}}})}{X}{j}{U} \; \wkEq \;
\hsubst{(\app{X}{\vec{V}})}{X}{j}{U}.
\]
\end{enumerate}
Let $\kindS{\gamma}{K}$, then
\begin{enumerate}[resume,nosep]
\item\label{item:hsubst-kds-etaexp} if
$\; \kindS{\gamma, X \kas \ksimp{K}, \delta}{J}$, then
$\hsubst{J}{X}{\ksimp{K}}{\etaExp{K}{X}} \; \wkEq \; J$;
\item\label{item:hsubst-nf-etaexp} if
$\; \gamma, X \kas \ksimp{K}, \delta \ts V \kin j$, then
$\hsubst{V}{X}{\ksimp{K}}{\etaExp{K}{X}} \; \wkEq \; V$;
\item\label{item:hsubst-sp-etaexp} if
$\; \spS{\gamma, X \kas \ksimp{K}, \delta}{j}{\vec{V}}{l}$, then
$\hsubst{\vec{V}}{X}{\ksimp{K}}{\etaExp{K}{X}} \; \wkEq \; \vec{V}$;
\item\label{item:etaexp-rapp-nf} if $\; K = \dfun{X}{K_1}{K_2}$,
$\; \gamma \tsNe N \kin \ksimp{K}$ and
$\; \gamma \ts V \kin \ksimp{K_1}$, then
$\; \rapp{\etaExp{K}{N}}{\ksimp{K}}{V} \; \wkEq \;
\etaExp{\hsubst{K_2}{X}{\ksimp{K_1}}{V}}{\app{N}{V}}$;
\item\label{item:etaexp-rapp-sp} if $\; \gamma \tsNe N \kin \ksimp{K}$
and $\spS{\gamma}{\ksimp{K}}{\vec{V}}{\kstar}$, then
$\rapp{\etaExp{K}{N}}{\ksimp{K}}{\vec{V}} \; \wkEq \; \app{N}{\vec{V}}$.
\end{enumerate}
\end{lemma}
\begin{corollary}\label{cor:etaexp-var-hsubst}
If $\; \kindS{\gamma, X \kas j, \delta}{K}$ and
$\; \gamma \ts U \kin j$, then
$\hsubst{(\etaExp{K}{X})}{X}{j}{U} \; \wkEq \; U$.
\end{corollary}

It is in this lemma that we see the true usefulness of weak equality.
While syntactic equality is too strict for this particular
commutativity property, using judgmental type and kind equality would
have forced us to formulate its premises in terms of declarative
kinding.  This would have resulted in a weaker lemma with a more
complicated proof.
In \Sec{weq-canon} we show that weak equations can be converted
into judgmental ones provided the related types or kinds are
well-kinded or well-formed, respectively.  Hence, weak equality
affords us a relatively straightforward proof of this lemma (and the
next) with a minimal overhead in complexity.

In the proof of \Lem{etaexp-hsubst}, we employ the following helper
They are proven separately by three easy inductions:
the first on the derivation of $K_1 \wkEq K_2$, the second on the
structure of the kind $K$, and the third on the derivation of
$\; \spS{\gamma}{j}{\vec{V}}{k}$.
\begin{lemma}\label{lem:weq-simpeq}
Weakly equal kinds have equal shapes.  If $K_1 \wkEq K_2$, then
\end{lemma}
\begin{lemma}\label{lem:etaexp-ne-hsubst-miss}
Let $X \neq Y$, then
\hsubst{(\etaExp{K}{\app{X}{\vec{D}}})}{Y}{j}{E} \; \alEq \;
\etaExp{\hsubst{K}{Y}{j}{E}}{\app{X}{(\hsubst{\vec{D}}{Y}{j}{E})}}
for any $K$, $\vec{D}$, $j$ and $E$.
\end{lemma}
\begin{lemma}\label{lem:rapp-sp-concat}
Let $\; \gamma \ts U \kin j$, $\spS{\gamma}{j}{\vec{V}}{k}$ and
$\spS{\gamma}{k}{\vec{W}}{l}$, then
\; \rapp{U}{j}{(\scons{\vec{V}}{\vec{W}})} \; \alEq \;
\rapp{(\rapp{U}{j}{\vec{V}})}{k}{\vec{W}}.
\end{lemma}

\begin{proof}[Proof of \Lem{etaexp-hsubst}]
All six parts are proven simultaneously by induction on the
structure of~$K$.
Parts~\Item{hsubst-kds-etaexp}--\Item{hsubst-sp-etaexp} proceed by
an inner induction on the simple formation and kinding derivations
for $J$, $V$ and $\vec{V}$, respectively.  We show a few key cases,
the remainder of the proof is routine.
\begin{itemize}
\item \emph{Part~\Item{etaexp-ne-hsubst}, $K = \dfun{Y}{K_1}{K_2}$.}
By inspection of the formation and kinding rules, we must have
$\kindS{\gamma, X \kas j, \delta}{K_1}$,
$\kindS{\gamma, X \kas j, \delta, Y \kas \ksimp{K_1}}{K_2}$ and
$\spS{\gamma, X \kas j, \delta}{j}{\vec{V}}{\ksimp{K}}$.
By \Lem{simp-hsubst} we have
\[ \gamma, \delta \ts \hsubst{(\app{X}{\vec{V}})}{X}{j}{U} \kin
\fun{\ksimp{K_1}}{\ksimp{K_2}} \qquad \text{and} \qquad
\kindS{\gamma, \delta}{\hsubst{K_1}{X}{j}{U}}.
\]
The final kinding rule used to derive the first of these judgments
must be~\ruleref{SK-Abs} since that is the only rule assigning
arrow shapes to normal types.  Therefore, the following must
hold for some $J$ and $W$:
\begin{align}
\hsubst{(\app{X}{\vec{V}})}{X}{j}{U} &= \lam{Y}{J}{W}
\label{eq:kind-gen1}\\
\ksimp{K_1} &= \ksimp{J} \label{eq:kind-gen2} \\
\gamma, \delta, Y \kas \ksimp{J} &\ts W \kin \ksimp{K_2}.
\label{eq:kind-gen3}
\end{align}
By weakening (\Lem{simp-weaken}), \Lem{sk-etaexp}
and~\ruleref{SK-NeApp} we also have
\[
\gamma, X \kas j, \delta, Y \kas \ksimp{K_1} \tsNe
\appp{X}{\vec{V}}{(\etaExp{K_1}{Y})} \kin \ksimp{K_2}
\] and hence
\begin{align*}
\hsubst{(\etaExp{K_2}{\appp{X}{\vec{V}}{(\etaExp{K_1}{Y})}})}{X}{j}{U}
\hspace{-10em}& \\
&\wkEq \;
\hsubst{(\appp{X}{\vec{V}}{(\etaExp{K_1}{Y})})}{X}{j}{U}
\tag{by IH for~\Item{etaexp-ne-hsubst}}\\
&\alEq \;
\rapp{U}{j}{(\hsubst{(\scons{\vec{V}}{(\etaExp{K_1}{Y})})}{X}{j}{U})}
\tag{by definition}\\
&\alEq \;
\rapp{(\rapp{U}{j}{(\hsubst{\vec{V}}{X}{j}{U})})}{
\ksimp{K}}{(\hsubst{(\etaExp{K_1}{Y})}{X}{j}{U})}
\tag{by \Lem[Lemmas]{hsubst-concat} and \ref{lem:rapp-sp-concat}}\\
&\alEq \;
\rapp{(\rapp{U}{j}{(\hsubst{\vec{V}}{X}{j}{U})})}{
\ksimp{K}}{(\etaExp{\hsubst{K_1}{X}{j}{U}}{Y})}
\tag{by \Lem{etaexp-ne-hsubst-miss}}\\
&\alEq \;
\rapp{(\hsubst{(\app{X}{\vec{V}})}{X}{j}{U})}{
\fun{\ksimp{K_1}}{\ksimp{K_2}}}{(\etaExp{\hsubst{K_1}{X}{j}{U}}{Y})}
\tag{by definition}\\
&\alEq \;
\rapp{(\lam{Y}{J}{W})}{
\fun{\ksimp{K_1}}{\ksimp{K_2}}}{(\etaExp{\hsubst{K_1}{X}{j}{U}}{Y})}
\tag{by \eqref{eq:kind-gen1}}\\
&\alEq \;
\hsubst{W}{Y}{\ksimp{K_1}}{(\etaExp{\hsubst{K_1}{X}{j}{U}}{Y})}
\tag{by definition}\\
&\wkEq \;
\tag{by~\Lem{weq-simpeq}, \eqref{eq:kind-gen3} and
IH for~\Item{hsubst-nf-etaexp}}
\end{align*}
We conclude that
\begin{align*}
\hsubst{(\etaExp{K}{\app{X}{\vec{V}}})}{X}{j}{U} \hspace{-6em}& \\
&\alEq \;
\lam{Y}{\hsubst{K_1}{X}{j}{U}}{
\hsubst{(\etaExp{K_2}{\appp{X}{\vec{V}}{
\tag{by definition}\\
&\wkEq \; \lam{Y}{J}{W}
\tag{by~\Lem{weq-simpeq}, \eqref{eq:kind-gen2},
the above and~\ruleref{WEq-Abs}}\\
&\alEq \; \hsubst{(\app{X}{\vec{V}})}{X}{j}{U}.
\tag{by~\eqref{eq:kind-gen1}}
\end{align*}

\item \emph{Part~\Item{hsubst-nf-etaexp}, case \ruleref{SK-Ne}.}
The rule~\ruleref{SK-Ne} has only one premise which must have been
derived using~\ruleref{SK-VarApp}, so $V = N = \app{Y}{\vec{V}}$
and we have
$\spS{\gamma, X \kas \ksimp{K}, \delta}{j}{\vec{V}}{\kstar}$ with
$(\gamma, X \kas \ksimp{K}, \delta)(Y) = j$.  We distinguish two
cases: $Y = X$ and $Y \neq X$ but consider only the first case
here; the second case is simpler.  Since $Y = X$, we have
$j = \ksimp{K}$, and
\begin{align*}
\hsubst{V&}{X}{\ksimp{K}}{\etaExp{K}{X}}\\
&\alEq \;
\rapp{\etaExp{K}{X}}{\ksimp{K}}{
\tag{by definition}\\
&\wkEq \;
\rapp{\etaExp{K}{X}}{\ksimp{K}}{\vec{V}}
\tag{by~reflexivity of $\wkEq$, IH for~\Item{hsubst-sp-etaexp}
and \Lem{weq-par-hsubst}.\Item{weq-rapp-sp}}\\
&\wkEq \;
\app{X}{\vec{V}}.
\tag{by \ruleref{SK-VarApp} and the IH for~\Item{etaexp-rapp-sp}}
\end{align*}
\item \emph{Part~\Item{etaexp-rapp-nf}, $K = \dfun{X}{K_1}{K_2}$.}
By inspection of the formation and kinding rules, we must have
$\kindS{\gamma}{K_1}$ and $N = \app{Y}{\vec{U}}$ with
\begin{align*}
\rapp{\etaExp{K}{N}}{\ksimp{K}}{V} &\alEq \;
\rapp{\lam{X}{K_1}{\etaExp{K_2}{\appp{Y}{\vec{U}}{(\etaExp{K_1}{X})}}}}{
\ksimp{K}}{V}
\tag{by definition}\\
&\alEq \;
\hsubst{\etaExp{K_2}{\appp{Y}{\vec{U}}{(\etaExp{K_1}{X})}}}{X}{
\ksimp{K_1}}{V}
\tag{by definition}\\
&\alEq \;
\etaExp{\hsubst{K_2}{X}{\ksimp{K_1}}{V}}{
\app{Y}{(\hsubst{(\scons{\vec{U}}{(\etaExp{K_1}{X})})}{X}{
\ksimp{K_1}}{V})}}
\tag{by \Lem{etaexp-ne-hsubst-miss}}\\
&\alEq \;
\etaExp{\hsubst{K_2}{X}{\ksimp{K_1}}{V}}{
\appp{Y}{\vec{U}}{(\hsubst{(\etaExp{K_1}{X})}{X}{
\ksimp{K_1}}{V})}}
\tag{as $X \notin \fv(\vec{U})$}\\
&\wkEq \;
\etaExp{\hsubst{K_2}{X}{\ksimp{K_1}}{V}}{
\appp{Y}{\vec{U}}{V}}.
\tag{by IH for \Item{etaexp-ne-hsubst} and \Lem{weq-etaexp}}
\end{align*}
\end{itemize}
The use of the IH in the last step corresponds to
\Cor{etaexp-var-hsubst}.
\end{proof}

\Lem{etaexp-hsubst} in place, we are ready to prove that normalization
weakly commutes with substitution.  In the following,
$\Gamma \wkEq \Delta$ denotes the pointwise lifting of weak equality
to contexts.
\begin{lemma}\label{lem:weq-nf-hsubst}
Substitution weakly commutes with normalization of well-formed kinds
and well-kinded types.  Let $\; \Gamma \ts A \kin J$ and
$V = \nf{\nfCtx{\Gamma}}{A}$, then
\begin{enumerate}
\item\label{item:weq-nf-hsubst-kd} if
$\; \kindD{\Gamma, X \kas J, \Delta}{K}$, then
$\nf{\nfCtx{\Gamma,\subst{\Delta}{X}{A}}}{\subst{K}{X}{A}} \;
\wkEq \;
\hsubst{(\nf{\nfCtx{\Gamma, X \kas J, \Delta}}{K})}{X}{\ksimp{J}}{V}$;
\item\label{item:weq-nf-hsubst-tp} if
$\; \Gamma, X \kas J, \Delta \ts B \kin K$, then
$\nf{\nfCtx{\Gamma,\subst{\Delta}{X}{A}}}{\subst{B}{X}{A}} \;
\wkEq \;
\hsubst{(\nf{\nfCtx{\Gamma, X \kas J, \Delta}}{B})}{X}{\ksimp{J}}{V}$;
\end{enumerate}
\end{lemma}
\begin{proof}
Simultaneously by induction on declarative kind formation and
kinding derivations.
In the case for~\ruleref{K-Var} where $B = Y$, we use
\Cor{etaexp-var-hsubst} if $Y = X$.
Otherwise, let $\Sigma = \Gamma, X \kas J, \Delta$ and
$\Sigma' = \Gamma, \subst{\Delta}{X}{A}$.
By stability of simplified contexts under normalization and
hereditary substitution, and by commutation of simplification and
context lookup, we have
\begin{align*}
\ksimp{\nfCtx{\Sigma'}(Y)}
&\; \alEq \;
\ksimp{\nfCtx{\Sigma'}}(Y)
\; \alEq \;
\ksimp{\Sigma'}(Y) \\
&\; \alEq \;
(\ksimp{\Gamma}, \ksimp{\subst{\Delta}{X}{A}})(Y)
\; \alEq \;
(\ksimp{\Gamma}, \ksimp{\Delta})(Y)
\; \alEq \;
(\ksimp{\Gamma}, X \kas \ksimp{J}, \ksimp{\Delta})(Y)
\; \alEq \;
\ksimp{\Sigma}(Y) \\
&\; \alEq \;
\ksimp{\nfCtx{\Sigma}}(Y)
\; \alEq \;
\ksimp{\nfCtx{\Sigma}(Y)}
\; \alEq \;
\ksimp{\nf{\Sigma}{\Sigma(Y)}}
\; \alEq \;
\ksimp{\hsubst{(\nf{\Sigma}{\Sigma(Y)})}{X}{\ksimp{J}}{V}}
\end{align*}
Hence, by \Lem{weq-etaexp} and \Lem{etaexp-ne-hsubst-miss} we have
\[
\etaExp{\nfCtx{\Sigma'}(Y)}{Y}
\; \wkEq \;
\etaExp{\hsubst{(\nf{\Sigma}{\Sigma(Y)})}{X}{\ksimp{J}}{V}}{Y}
\; \alEq \;
\hsubst{(\etaExp{\nf{\Sigma}{\Sigma(Y)}}{Y})}{X}{\ksimp{J}}{V}.
\]
In the case for~\ruleref{K-App}, we use
\Lem{weq-par-hsubst}.\Item{weq-hsubst-elim} and
\Lem{hsubst-comm}.\Item{hsubst-comm-nf}.
\end{proof}

The very last lemma of this section will be used in our equivalence
proof in \Sec{canon-complete-full} to show that subtyping rules for
$\eta$-conversion of normal operators are admissible in canonical
\begin{lemma}\label{lem:weq-nf-etaexp}
If $\; \Gamma \ts A \kin \dfun{X}{J}{K}$ with $X \notin \fv(A)$,
$\nf{\nfCtx{\Gamma}}{\lam{X}{J}{\app{A}{X}}} \wkEq
\nf{\nfCtx{\Gamma}}{A}$.
\end{lemma}
\begin{proof}
The proof uses \Lem{nf-simp} to obtain
$\; \ksimp{\nfCtx{\Gamma}} \ts \nf{\nfCtx{\Gamma}}{A} \kin
\fun{\ksimp{J}}{\ksimp{K}}$
and proceeds by case analysis on the final rule used to derive this
simple kinding judgment; the only applicable rule
is~\ruleref{SK-Abs}.  The remainder of the proof uses equational
reasoning very similar to that used in the proof of
\Lem{etaexp-hsubst}.\Item{etaexp-ne-hsubst}.
\end{proof}

\section{Properties of the Canonical System}
\label{sec:canon_basics}

This section states and proves some basic yet important metatheoretic
properties of the canonical system that have been omitted from
\Sec{canonical} of the paper.
As a first step, we prove soundness of the canonical
system in \Sec{canon-sound-full}.
Next, we state and prove a \emph{hereditary substitution lemma} in
\Sec{canon-hsubst-full}, which establishes that canonical judgments
are preserved by hereditary substitutions.
This lemma is a key ingredient in proving completeness of the
canonical system.
We prove completeness in \Sec{canon-complete-full}, after showing that
canonical subtyping can be inverted at the top-level in
\Sec{canon-inversion-full}.
\Fig{canon_rules_sup} shows the canonical judgments that have been
omitted from the paper: context and kind formation, subkinding, and
kind and type equality.

\fig{fig:canon_rules_sup}{Canonical presentation of \FOmegaInt{} -- supplement}{
\judgment{Context formation}{\fbox{$\ctxC{\Gamma}$}}

\bigskip

\begin{minipage}[t]{0.21\linewidth}
\infrule[\ruledef{CC-Empty}]{\quad}{\ctxC{\cempty}}
\end{minipage}\hspace{1ex}
\begin{minipage}[t]{0.35\linewidth}
\infrule[\ruledef{CC-TmBind}]
{\ctxC{\Gamma} \quad \kindC{\Gamma}{K}}
{\ctxC{\Gamma, X \kas K}}
\end{minipage}\hfill
\begin{minipage}[t]{0.40\linewidth}
\infrule[\ruledef{CC-TpBind}]
{\ctxC{\Gamma} \quad \typeC{\Gamma}{V}}
{\ctxC{\Gamma, x \tas V}}
\end{minipage}

\bigskip

\judgment{Kind formation}{\fbox{$\kindC{\Gamma}{K}$}}

\bigskip

\begin{minipage}[t]{0.52\linewidth}
\infruleLeft{CWf-Intv}
{\typeC{\Gamma}{U} \andalso \typeC{\Gamma}{V}}
{\kindC{\Gamma}{U \intv V}}
\end{minipage}\hfill
\begin{minipage}[t]{0.46\linewidth}
\infruleLeft{CWf-DArr}
{\kindC{\Gamma}{J} \andalso \kindC{\Gamma, X \kas J}{K}}
\end{minipage}

\bigskip

\judgment{Subkinding}{\fbox{$\Gamma \ts J \ksub K$}}

\bigskip

\begin{minipage}[t]{0.44\linewidth}
\infruleLeft{CSK-Intv}
\Gamma \ts U_2 \tsub U_1  \andalso  \Gamma \ts V_1 \tsub V_2}
{\Gamma \ts U_1 \intv V_1 \ksub U_2 \intv V_2}
\end{minipage}\hspace{1ex}
\begin{minipage}[t]{0.54\linewidth}
\infruleLeft{CSK-DArr}
\Gamma \ts J_2 \ksub J_1  \andalso
\Gamma, X \kas J_2 \ts K_1 \ksub K_2}
{\Gamma \ts \dfun{X}{J_1}{K_1} \ksub \dfun{X}{J_2}{K_2}}
\end{minipage}

\bigskip

\begin{minipage}[2]{0.4\linewidth}
\judgment{Kind equality}{\fbox{$\Gamma \ts J \keq K$}}

\infruleLeft{CSK-AntiSym}
{\kind{\Gamma}{J}      \andalso  \kind{\Gamma}{K}\\
\Gamma \ts J \tsub K  \andalso  \Gamma \ts K \tsub J}
{\Gamma \ts J \teq K}
\end{minipage}\hspace{0.07\linewidth}
\begin{minipage}[2]{0.5\linewidth}
\judgment{Type equality}{\fbox{$\Gamma \ts U \keq V \kck K$}}

\infruleLeft{CST-AntiSym}
\Gamma \ts U \tsub V \kck K  \andalso  \Gamma \ts V \tsub U \kck K}
{\Gamma \ts U \teq V \kck K}
\end{minipage}}

The contents of this section are based on Chapter~5 of the first
author's PhD~dissertation.  We refer the interested reader to the
dissertation for the full details~\cite[][Ch.~5]{Stucki17thesis}.

\subsection{Soundness and Basic Properties}
\label{sec:canon-sound-full}

Before we establish any other metatheoretic properties of the
canonical system, let us prove its soundness with respect to the
declarative presentation.  To avoid confusion, we mark canonical
judgments with the subscript ``$\mathsf{c}$'' and declarative ones
with ``$\mathsf{d}$'' in the following lemma.

\begin{lemma}[soundness of the canonical rules]
\label{lem:canon-sound-full}
\begin{enumerate}[nosep]
\item\label{item:can-snd-ctx} If $\; \ctxCC{\Gamma}$, then
$\; \ctxDD{\toType{\Gamma}}$.
\item\label{item:can-snd-kd} If $\; \kindCC{\Gamma}{K}$, then
$\; \kindDD{\toType{\Gamma}}{\toType{K}}$.
\item\label{item:can-snd-sk} If $\; \Gamma \tsC J \ksub K$, then
$\; \toType{\Gamma} \tsD \toType{J} \ksub \toType{K}$.
\item\label{item:can-snd-keq} If $\; \Gamma \tsC J \keq K$, then
$\; \toType{\Gamma} \tsD \toType{J} \keq \toType{K}$.
\item\label{item:can-snd-var} If $\; \Gamma \tsVar X \kin K$, then
$\; \toType{\Gamma} \tsD X \kin \toType{K}$.
\item\label{item:can-snd-ne} If $\; \Gamma \tsNe N \kin K$, then
$\; \toType{\Gamma} \tsD \toType{N} \kin \toType{K}$.
\item\label{item:can-snd-nfsn} If $\; \Gamma \tsC V \ksn K$, then
$\; \toType{\Gamma} \tsD \toType{V} \kin \toType{K}$.
\item\label{item:can-snd-nfck} If $\; \Gamma \tsC V \kck K$, then
$\; \toType{\Gamma} \tsD \toType{V} \kin \toType{K}$.
\item\label{item:can-snd-st} If $\; \Gamma \tsC U \tsub V$, then
$\; \toType{\Gamma} \tsD \toType{U} \tsub \toType{V} \kin \kstar$.
\item\label{item:can-snd-stck} If $\; \Gamma \tsC U \tsub V \kin K$, then
$\; \toType{\Gamma} \tsD \toType{U} \tsub \toType{V} \kin
\toType{K}$.
\item\label{item:can-snd-teq} If $\; \Gamma \tsC U \teq V \kin K$, then
$\; \toType{\Gamma} \tsD \toType{U} \tsub \toType{V} \kin
\toType{K}$.
\item\label{item:can-snd-sp} If
$\; \toType{\Gamma} \tsD A \kin \toType{J}$ and
$\; \spCC{\Gamma}{J}{\vec{V}}{K}$, then
$\; \toType{\Gamma} \tsD \toType{\app{\toElim{A}}{\vec{V}}} \kin
\toType{K}$.
\item\label{item:can-snd-speq} If
$\; \toType{\Gamma} \tsD A \tsub B \kin \toType{J}$ and
$\; \spCC{\Gamma}{J}{\vec{U} \teq \vec{V}}{K}$, then
$\; \toType{\Gamma} \tsD \toType{\app{\toElim{A}}{\vec{U}}} \tsub
\toType{\app{\toElim{B}}{\vec{V}}} \kin \toType{K}$.
\end{enumerate}
\end{lemma}
The proof uses the following two helper lemmas.
The first is a derived rule, the second is proven by easy case
analysis of the rules for kind synthesis.
\begin{lemma}\label{lem:K-Intv-Star}
If $\; \Gamma \ts A \kin B \intv C$, then also
$\Gamma \ts A \kin \kstar$.
\end{lemma}\noindent
\begin{lemma}\label{lem:nfsn-intv-sing}
If $\; \Gamma \ts U \ksn V \intv W$, then $V \alEq U$ and
$W \alEq U$.
\end{lemma}\noindent
\begin{proof}[Proof of \Lem{canon-sound-full}]
By induction on derivations of the various canonical judgments; for
parts~\Item{can-snd-ctx}--\Item{can-snd-teq}, on the derivation of
the first premise, for parts~\Item{can-snd-sp}
and~\Item{can-snd-speq}, on that of the second premise.  Most cases
are straightforward.  In cases involving synthesized kinding of
proper types, we use~\ruleref{K-Sing} and \Lem[Lemmas]{K-Intv-Star},
\ref{lem:ST-Intv-Star} and~\ref{lem:nfsn-intv-sing} to adjust kinds
where necessary.  In cases involving hereditary substitutions, i.e.\
those for~\ruleref{CK-Cons} and~\ruleref{SpEq-Cons}, we use
soundness of hereditary substitution in kinds
\end{proof}

As for the declarative system, the contexts of most canonical
judgments are well-formed.  There are two exceptions: kinding and
equality of spines. The rules~\ruleref{CK-Empty}
and~\ruleref{SpEq-Empty} for empty spines offer no guarantee that the
enclosing context is well-formed.  This is not a problem in practice,
since well-kinded spines only appear in judgments about neutral types,
the heads of which must be kinded in a well-formed context.
\begin{lemma}[context validity]\label{lem:canon_ctx_valid}
Assume $\; \judgD{\Gamma}$ for any canonical judgment except spine
kinding or equality.  Then $\; \ctxD{\Gamma}$.
\end{lemma}
\begin{proof}
By simultaneous induction on the derivations of the various
\end{proof}
We can prove a few more validity properties at this point.
First, since synthesized kinds are singletons, validity of synthesized
kinding judgments follows by~\ruleref{CWf-Intv} for proper types and
by an easy induction for type operators.
Second, validity of kind equality as well as the checked subtyping and
type equality judgments follows immediately from the validity
conditions included in the rules~\ruleref{CSK-AntiSym},
\ruleref{CST-Intv}, \ruleref{CST-Abs} and~\ruleref{CST-AntiSym}.
\begin{lemma}[canonical validity -- part 1]\label{lem:canon-valid1}
\begin{enumerate}[nosep,leftmargin=14.85em,labelsep=.9em]
\item[(synthesized kinding validity)]
If $\; \Gamma \ts V \ksn K$, then $\kindC{\Gamma}{K}$.

\item[(checked subtyping validity)]
If $\; \Gamma \ts U \tsub V \kck K$, then $\Gamma \ts U \kck K$ and
$\Gamma \ts V \kck K$.

\item[(kind equation validity)]
If $\; \Gamma \ts J \keq K$, then $\kindC{\Gamma}{J}$ and

\item[(type equation validity)]
If $\; \Gamma \ts U \teq V \kck K$, then $\Gamma \ts U \kck K$,
$\; \Gamma \ts V \kck K$ and $\kindC{\Gamma}{K}$.
\end{enumerate}
\end{lemma}
We prove the remaining validity properties of the canonical system
in~\Sec{canon-valid}, once we have shown that hereditary substitutions
preserve well-formedness of kinds.

Before we can do so, we need to establish the usual weakening and
context narrowing lemmas for canonical typing.
\begin{lemma}[weakening]\label{lem:canon-weaken}
Assume $\; \judgC{\Gamma, \Delta}$ for any of the canonical
\begin{enumerate}
\item If $\; \typeC{\Gamma}{A}$, then
$\; \judgC{\Gamma, x \tas A, \Delta}$.
\item If $\; \kindC{\Gamma}{K}$, then
$\; \judgC{\Gamma, X \kas K, \Delta}$.
\end{enumerate}
\end{lemma}

\begin{corollary}[iterated weakening]\label{cor:canon-iter-weaken}
If $\; \ctxC{\Gamma, \Delta}$ and $\judgC{\Gamma}$, then
$\judgC{\Gamma, \Delta}$.
\end{corollary}

\begin{lemma}[context narrowing -- weak version]\label{lem:canon-weak-narrow}
\begin{enumerate}
\item If $\; \typeC{\Gamma}{A}$, $\; \Gamma \ts A \tsub B \kin \kstar$
and $\; \judgC{\Gamma, x \tas B, \Delta}$, then
$\; \judgC{\Gamma, x \tas A, \Delta}$.
\item If $\; \kindC{\Gamma}{J}$, $\; \Gamma \ts J \ksub K$ and
$\; \judgC{\Gamma, X \kas K, \Delta}$, then
$\; \judgC{\Gamma, X \kas J, \Delta}$.
\end{enumerate}
\end{lemma}

The proofs of both lemmas are routine inductions on the derivations of
the respective judgments.  The proof of context narrowing is only easy
thanks to the rule~\ruleref{CV-Sub}.  Without this rule, the canonical
kinding judgments for variables and neutral types would become
synthesis judgments and context narrowing would no longer hold in its
present form for these two judgments.  To see this, consider the
variable kinding judgment $\Gamma, X \kas K, \Delta \tsVar X \kin K$,
which, after eliminating~\ruleref{CV-Sub}, could only be derived
using~\ruleref{CV-Var}.  If we were to narrow the context by changing
the declared kind $K$ of $X$ to some $J$ such that
$\Gamma \ts J \ksub K$, then the synthesized kind of $X$ would
necessarily change to $J$ too.

For neutral kinding, we would be in a similar situation as the new
synthesized kind of the head would have to be propagated through the
kinding derivation of the spine.  Along the way, the new kind $J$
would have to be unraveled by repeatedly separating
$J = \dfun{X}{J_1}{J_2}$ into $J_1$, $J_2$ and hereditarily
substituting the next element of the spine into the codomain $J_2$.
To prove context narrowing for the remainder of the canonical
judgments, we would have to maintain the invariant that the new
synthesized kind of a neutral type is a subtype of the original one,
i.e. if $\; \Gamma, X \kas K_1, \Delta \tsVar N \ksn K_2$ and
$\Gamma \ts J_1 \ksub K_1$ then
$\Gamma, X \kas J_1, \Delta \tsVar N \ksn J_2$ and
$\Gamma \ts J_2 \ksub K_2$.  Because spine kinding involves hereditary
substitution, a proof involving this invariant would require a
hereditary substitution lemma for subtyping, i.e.\ a proof that
hereditary substitutions preserve subtyping.  We give such a proof in
\Sec{canon-hsubst-full} and, as we will see there, it makes crucial use of
context narrowing itself.  By allowing us to establish
\Lem{canon-weak-narrow} independently, the rule~\ruleref{CV-Sub} thus
simplifies the proof of an otherwise rather complicated lemma (see
\Lem{canon-hsubst-full} for details).

\subsubsection{Order-Theoretic Properties}
\label{sec:canon-order}

Having established context narrowing, we can prove the usual
order-theoretic properties of canonical subkinding, subtyping, as well
as kind and type equality.  We start by stating an proving the various
reflexivity properties which, unlike those for the declarative
relations, have to be proven simultaneously for the canonical

\begin{lemma}\label{lem:canon-refl}
The following reflexivity rules are all admissible.
\end{lemma}
\begin{multicols}{2}
\typicallabel{CSK-ReflSub}
\infrule[\ruledef{CSK-Refl}]
{\Gamma \ts K \ksub K}

\infrule[\ruledef{CST-ReflSyn}]
{\Gamma \ts U \ksn V \intv W}
{\Gamma \ts U \tsub U}

\infrule[\ruledef{CKEq-Refl}]
{\Gamma \ts K \keq K}

\infrule[\ruledef{CST-ReflCk}]
{\Gamma \ts V \kck K  \andalso  \kindC{\Gamma}{K}}
{\Gamma \ts V \tsub V \kck K}
\end{multicols}
\vspace{.1pt}

\infrule[\ruledef{CST-ReflSub}]
{\Gamma \ts V \ksn J  \andalso  \Gamma \ts J \ksub K  \andalso
\kindC{\Gamma}{K}}
{\Gamma \ts V \tsub V \kck K}
\vspace{.1pt}

\begin{multicols}{2}
\infrule[\ruledef{SpEq-Refl}]
{\spC{\Gamma}{J}{\vec{V} \keq \vec{V}}{K}}

\infrule[\ruledef{CTEq-Refl}]
{\Gamma \ts V \kck K  \andalso  \kindC{\Gamma}{K}}
{\Gamma \ts V \teq V \kck K}
\end{multicols}
\begin{proof}
The proof is by mutual induction in the structure of the kinds and
types being related to themselves, and then by case-analysis on the
final rules of the corresponding kind formation and kinding
derivations.  The proof for~\ruleref{CST-ReflSub} proceeds by an
inner induction on the derivation of $\Gamma \ts J \ksub K$.  In the
case for~\ruleref{CSK-DArr} where $V = \lam{X}{J_1}{U}$ and we have
$\Gamma \ts K_1 \ksub J_1$, $\Gamma, X \kas K_1 \ts J_2 \ksub K_2$
and $\Gamma, X \kas J_1 \ts U \ksn J_2$, we use context narrowing to
adjust the declared kind of $X$ from $J_1$ to $K_1$ in
$\; \Gamma, X \kas J_1 \ts U \ksn J_2$ before applying the IH to
obtain $\Gamma, X \kas K_1 \ts U \tsub U \kck K_2$.
\end{proof}
Transitivity of the various relations and symmetry of the equalities
are more easily established, thanks to the rule~\ruleref{CST-Trans} on
the one hand, and to the structure of equality on the other.
\begin{lemma}\label{lem:canon-trans}
Canonical subkinding, subtyping, kind and type equality are
\end{lemma}
\begin{multicols}{2}
\typicallabel{CKEq-Trans}
\infrule[\ruledef{CSK-Trans}]
{\Gamma \ts J \ksub K  \andalso  \Gamma \ts K \ksub L}
{\Gamma \ts J \ksub L}

\infrule[\ruledef{CKEq-Trans}]
{\Gamma \ts J \keq K  \andalso  \Gamma \ts K \keq L}
{\Gamma \ts J \keq L}
\end{multicols}
\begin{multicols}{2}
\infrule[\ruledef{CST-TransCk}]
{\Gamma \ts U \tsub V \kck K  \andalso  \Gamma \ts V \tsub W \kck K}
{\Gamma \ts U \tsub W \kck K}

\infrule[\ruledef{CTEq-Trans}]
{\Gamma \ts U \teq V \kck K  \andalso  \Gamma \ts V \teq W \kck K}
{\Gamma \ts U \teq W \kck K}
\end{multicols}
\begin{proof}
The proof of~\ruleref{CSK-Trans} is by induction on the structure of
$K$ and case analysis on the final rules used to derive the
premises.  In the case for $K = \dfun{X}{K_1}{K_2}$ we use context
narrowing.  The proof of~\ruleref{CST-Trans} is by induction on the
derivation of the first premise.  The proofs of~\ruleref{CKEq-Trans}
and~\ruleref{CTEq-Trans} are by inspection of the equality rules and
use~\ruleref{CSK-Trans} and~\ruleref{CST-Trans}, respectively.
\end{proof}

\begin{lemma}\label{lem:canon-sym}
Canonical kind and type equality are symmetric.
\begin{multicols}{2}\normalfont
\typicallabel{CKEq-Sym}
\infrule[\ruledef{CKEq-Sym}]
{\Gamma \ts J \keq K}
{\Gamma \ts K \keq J}

\infrule[\ruledef{CTEq-Sym}]
{\Gamma \ts U \keq V \kck K}
{\Gamma \ts V \keq U \kck K}
\end{multicols}
\end{lemma}
\begin{proof}
By inspection of the equality rules, \ruleref{CSK-AntiSym}
\end{proof}

Thanks to context narrowing and subkinding transitivity, we can prove
admissibility of the following subsumption rules for the three checked
\begin{lemma}
Kind subsumption is admissible in the checked judgments.
\end{lemma}
\begin{center}
\infruleSimp[CK-SubCk]
{\Gamma \ts U \kck J  \andalso  \Gamma \ts J \ksub K}
{\Gamma \ts U \kck K}
\hspace{2em}
\infruleSimp[CST-SubCk]
{\Gamma \ts U \tsub V \kck J  \andalso  \Gamma \ts J \ksub K}
{\Gamma \ts U \tsub V \kck K}

\infruleSimp[CTEq-SubCk]
{\Gamma \ts U \teq V \kck J  \andalso  \Gamma \ts J \ksub K}
{\Gamma \ts U \teq V \kck K}
\end{center}
\begin{proof}
Admissibility is proven separately for the three rules, in the order
they are listed.  The proof of~\ruleref{CK-SubCk} is by inspection
of the kind checking rules
and uses~\ruleref{CSK-Trans}.  The proof of~\ruleref{CST-SubCk} is
by induction on the derivation of the second premise
$\Gamma \ts J \ksub K$ and uses~\ruleref{CK-SubCk} as well as context
narrowing for the inductive step.  The proof of~\ruleref{CTEq-SubCk}
is by inspection of the equality rules and uses~\ruleref{CST-SubCk}.
\end{proof}

Kind subsumption subsumes kind conversion thanks to the first of the
following three rules, all of which follow immediately by inspection
of the equality and checked subtyping rules.
\begin{center}
\infruleSimp[CSK-Refl-KEq]
{\Gamma \ts J \keq K}
{\Gamma \ts J \tsub K}
\hspace{2em}
\infruleSimp[CST-Refl-TEq]
{\Gamma \ts U \teq V \kck K}
{\Gamma \ts U \tsub V \kck K}

\infruleSimp[CST-Refl-TEq']
{\Gamma \ts U \teq V \kck W \intv W'}
{\Gamma \ts U \tsub V}
\end{center}

\subsubsection{Canonical Replacements for Declarative Rules}
\label{sec:canon-admissible}

Our completeness proof for the canonical system relies on the fact
that the normal form $\nf{}{A}$ of any declaratively well-kinded type
$\Gamma \ts A \kin K$ kind checks against the normal form $\nf{}{K}$
of the corresponding kind $K$, i.e.\ that we have
$\nfCtx{\Gamma} \ts \nf{}{A} \kck \nf{}{K}$.  To simplify the proof of
this fact, we establish a set of admissible kind checking rules below
that mirror the corresponding declarative rules.

We begin by proving that normal forms with synthesized or checked
interval kinds also check against~$\kstar$.
\begin{lemma}\label{lem:CK-Intv-Star}
Types inhabiting interval kinds are proper types.  If
$\; \Gamma \ts U \ksn V \intv W$ or
$\; \Gamma \ts U \kck V \intv W$, then also
$\Gamma \ts U \kck \kstar$.
\end{lemma}
\begin{proof}
If $\; \Gamma \ts U \ksn V \intv W$, then by~\Lem{nfsn-intv-sing},
$\; \Gamma \ts U \ksn U \intv U$.  From this we derive the result
by~\ruleref{CST-Bot}, \ruleref{CST-Top}, \ruleref{CSK-Intv}
and~\ruleref{CK-Sub}.  If $\; \Gamma \ts U \kck V \intv W$, then
this must have been derived using~\ruleref{CK-Sub} and hence
$\; \Gamma \ts U \ksn K$ and $\Gamma \ts K \ksub V \intv W$.  By
inspection of the subkinding rules, $K = V' \intv W'$ for some $V'$
and $W'$.  The result then follows by the first part of the lemma.
\end{proof}

The second part of the proof follows a pattern that is is quite
typical for proofs in the remainder of this section.  Thanks to the
division of kinding into kind synthesis and checking, and thanks to
the simplicity of both kind checking and subkinding derivations, we
can often prove properties of kind checking judgments
$\Gamma \ts U \kck K$ by appealing to similar properties of kind
synthesis judgments $\Gamma \ts U \ksn K'$ where $K$ and $K'$ have the
same shape, i.e. where $K$ and $K'$ are either both intervals or both
arrows.  Two more examples of this pattern appear in the following
lemma, where the admissibility proofs of the
and~\rulerefN{CST-CkBnd2}{CST-CkBnd$_2$}, which have kind checking
judgments as their premises, appeal to instances
and~\rulerefN{CST-SynBnd2}{CST-SynBnd$_2$}, respectively, which have
similar kind synthesis judgments as their premises.

\begin{lemma}\label{lem:canon-admissible}
All of the following are admissible.
\end{lemma}
\begin{multicols}{3}
\typicallabel{}
\infrule[\ruledef{CK-Sing'}]
{\Gamma \ts U \kck V \intv W}
{\Gamma \ts U \ksn U \intv U}

\infrule[\ruledef{CK-SynCk}]
{\Gamma \ts V \ksn K}
{\Gamma \ts V \kck K}

\infrule[\ruledef{CK-NeCk}]
{\Gamma \tsNe N \kin U \intv V}
{\Gamma \ts N \kck U \intv V}
\end{multicols}
\begin{multicols}{2}
\typicallabel{CST-SynBnd$_1$}
\infrule[\ruledef{CK-Arr'}]
{\typeCCk{\Gamma}{U}  \andalso  \typeCCk{\Gamma}{V}}

\infrule[\ruledef{CK-All'}]
{\kindC{\Gamma}{K}  \andalso  \typeCCk{\Gamma, X \kas K}{V}}
\end{multicols}
\begin{multicols}{2}
\typicallabel{CST-SynBnd$_1$}
\infrule[\ruledef{CK-Abs'}]
{\kindC{\Gamma}{J}  \andalso  \Gamma, X \kas J \ts V \kck K}
{\Gamma \ts \lam{X}{J}{V} \kck \dfun{X}{J}{K}}

\infrule[\ruledef{CST-Intv'}]
{\Gamma \ts V_1 \tsub V_2  \kck U \intv W}
{\Gamma \ts V_1 \tsub V_2 \kck V_1 \intv V_2}
\end{multicols}
\begin{multicols}{2}
\typicallabel{CST-SynBnd$_1$}
\infrule[\ruledefN{CST-SynBnd1}{CST-SynBnd$_1$}]
{\Gamma \ts U \ksn V_1 \intv V_2}
{\Gamma \ts V_1 \tsub U}

\infrule[\ruledefN{CST-CkBnd1}{CST-CkBnd$_1$}]
{\Gamma \ts U \kck V_1 \intv V_2}
{\Gamma \ts V_1 \tsub U}

\infrule[\ruledefN{CST-SynBnd2}{CST-SynBnd$_2$}]
{\Gamma \ts U \ksn V_1 \intv V_2}
{\Gamma \ts U \tsub V_2}

\infrule[\ruledefN{CST-CkBnd2}{CST-CkBnd$_2$}]
{\Gamma \ts U \kck V_1 \intv V_2}
{\Gamma \ts U \tsub V_2}
\end{multicols}
\vspace{.1pt}

\typicallabel{SpEq-Snoc}
\infrule[\ruledef{CK-Snoc}]
{\spC{\Gamma}{J}{\vec{U}}{\dfun{X}{K}{L}}  \andalso
\Gamma \ts V \kck K  \andalso  \kindC{\Gamma}{K}}

\infrule[\ruledef{SpEq-Snoc}]
{\spC{\Gamma}{J}{\vec{U}_1 \keq \vec{U}_2}{\dfun{X}{K}{L}}  \andalso
\Gamma \ts V_1 \keq V_2 \kck K}
{\spC{\Gamma}{J}{\scons{\vec{U}_1}{V_1} \keq \scons{\vec{U}_2}{V_2}}{\hsubst{L}{X}{\ksimp{K}}{V_1}}}

\begin{proof}
Some of the rules are derivable others are admissible; most of the
proofs are straightforward, so we omit the details.  The proofs of
the alternate type formation rules use~\ruleref{CK-Sing'} and
\Lem{CK-Intv-Star}.  The proofs of the alternate projection
and~\rulerefN{CST-SynBnd2}{CST-SynBnd$_2$} use \Lem{nfsn-intv-sing}
and reflexivity; those of~\rulerefN{CST-CkBnd1}{CST-CkBnd$_1$}
and~\rulerefN{CST-CkBnd2}{CST-CkBnd$_2$} are by inspection of kind
checking and subkinding and
and~\rulerefN{CST-SynBnd2}{CST-SynBnd$_2$}, respectively.  The
proofs of the last two rules are by induction on the derivations of
the respective first premises.
\end{proof}

As in the declarative system, we define \emph{canonical context
equality} $\ctxEqC{\Gamma}{\Delta}$ as the pointwise lifting of
canonical type and kind equality to context bindings:
\begin{center}
\infruleSimp{\quad}{\ctxEqD{\cempty}{\cempty}}
\hspace{3em}
\infruleSimp
{\ctxEqD{\Gamma}{\Delta} \andalso \Gamma \ts J \keq K}
{\ctxEqD{\Gamma, X \kas J}{\Delta, X \kas K}}
\hspace{3em}
\infruleSimp
{\ctxEqD{\Gamma}{\Delta} \andalso \Gamma \ts U \teq V \kck W \intv W'}
{\ctxEqD{\Gamma, x \tas U}{\Delta, x \tas V}}
\end{center}

\subsubsection{Simplification of Canonical Kinding}

In \Sec{simple_nf} of the previous section, we showed that every
well-formed kind and well-kinded type has a simply well-formed or
simply well-kinded normal form, respectively (see \Lem{nf-simp}).
Canonically well-formed kinds and canonically well-kinded types are
already in normal form, but we can still simplify their kind formation
and kinding derivations, as the following pair of lemma shows.  In the
statement of the second lemma, we use the subscript ``$\mathsf{nes}$''
to mark simple kinding judgments for neutral types and
``$\mathsf{ne}$'' to mark their canonical counterparts.
\begin{lemma}\label{lem:st-teq-simp}
Canonical subkinds and equal kinds simplify equally.  If
$\; \Gamma \ts J \tsub K$ or $\; \Gamma \ts J \teq K$ then
\end{lemma}
\begin{proof}
Separately, by induction on subkinding and kind equality
derivations, respectively.
\end{proof}
\begin{lemma}[simplification]\label{lem:canon-simp}
Well-formed kinds and well-kinded normal forms, neutrals and spines
are also simply well-formed and well-kinded, respectively.
\begin{enumerate}[nosep]
\item\label{item:canon-simp-var} If $\; \Gamma \tsVar X \kin K$, then
$\; \ksimp{\Gamma} \ts[nes] X \kin \ksimp{K}$.
\item\label{item:canon-simp-kd} If $\; \kindC{\Gamma}{K}$, then
$\; \kindS{\ksimp{\Gamma}}{K}$.
\item\label{item:canon-simp-ne} If $\; \Gamma \tsNe N \kin K$, then
$\; \ksimp{\Gamma} \ts[nes] N \kin \ksimp{K}$.
\item\label{item:canon-simp-sn} If $\; \Gamma \ts V \ksn K$, then
$\; \ksimp{\Gamma} \ts V \kin \ksimp{K}$.
\item\label{item:canon-simp-ck} If $\; \Gamma \ts V \kck K$, then
$\; \ksimp{\Gamma} \ts V \kin \ksimp{K}$.
\item\label{item:canon-simp-sp} If $\; \spC{\Gamma}{J}{\vec{V}}{K}$,
then $\; \spS{\ksimp{\Gamma}}{\ksimp{J}}{\vec{V}}{\ksimp{K}}$.
\end{enumerate}
\end{lemma}
\begin{proof}
Part~\Item{canon-simp-var} is proven separately,
parts~\Item{canon-simp-kd}--\Item{canon-simp-sp} are proven
simultaneously, all by induction on the derivations of the
respective premises.  The cases of~\ruleref{CV-Sub}
and~\ruleref{CK-Sub} use of \Lem{st-teq-simp}.
\end{proof}
Thanks to \Lem{canon-simp}, properties of simply kinded normal forms
still hold for canonically kinded normal forms.  For example,
by~\Lem[Lemmas]{canon-simp} and~\ref{lem:hsubst-comm}, hereditary
substitutions in canonically kinded types commute.

\subsection{The Hereditary Substitution Lemma}
\label{sec:canon-hsubst-full}

We have arrived at
the core of the technical development of this section: the proof of
the \emph{hereditary substitution lemma}.  The hereditary substitution
lemma states, roughly, that canonical judgments are preserved by
hereditary substitutions of canonically well-kinded types.  Just as
the ordinary substitution lemma for the declarative system
played a key role in the proofs of several metatheoretic properties
in \Sec{declarative} of the paper,
the hereditary substitution lemma is key to
proving important metatheoretic properties of the canonical system.
But unlike that of its ordinary counterpart, the proof of the
hereditary substitution lemma is rather challenging.  This is
reflected already in the statement of the lemma, which
features \Item{can-rapp-teq} separate parts, all of which have to be
proven simultaneously (see \Lem{canon-hsubst-full} below).

One reason for the large number of parts is simply that there are more
judgment forms in the canonical system than there are in the