@@ -189,6 +189,16 @@ The subjection conversion property is a generalization of a subject reduction in

\emph{subject conversion} and \emph{typability preservation} together

imply the \emph{subject reduction} property.

\end{lemma}

\begin{proof}

The idea, is to be able to use the \textsc{conv} rule to deduce this property.

We want to prove that \(\Gamma\vdash t_2 : A\) from the fact that \(t_1\hookrightarrow t_2\) and \(\Gamma\vdash t_1 : A\).

We use the \emph{typability preservation} property to get a type \(B\) to \(t_2\). Then, from the \emph{subject conversion} property, we know that \(\Gamma\vdash A \convbg B\).

The only thing we need now to apply the \textsc{conv} rule is to show that \(\Gamma\vdash A : s\) for some sort \(s\). However, this is not possible in general, for example when \(A =\tkind\). We have two cases to prove:

\begin{itemize}

\item If \(A =\tkind\), then using Lemma TODO, we can show that \(B =\tkind\), hence subject reduction is satisfied

\item If \(A \neq\tkind\), because \(A\) is inhabited, we can use Lemma TODO to conclude that \(\Gamma\vdash A :s\). Hence we can apply the \textsc{conv}, this closes the proof.

\end{itemize}

\end{proof}

\begin{lemma}[Type convertibility]

For all well-formed context $\Gamma$ satisfying

...

...

@@ -210,16 +220,6 @@ The subjection conversion property is a generalization of a subject reduction in

For any well-formed context \(\Gamma\), and term $t$ such that \(\tkind\convbg t\) then \(t =\tkind\).

\end{lemma}

\begin{proof}

The idea, is to be able to use the \textsc{conv} rule to deduce this property.

We want to prove that \(\Gamma\vdash t_2 : A\) from the fact that \(t_1\hookrightarrow t_2\) and \(\Gamma\vdash t_1 : A\).

We use the \emph{typability preservation} property to get a type \(B\) to \(t_2\). Then, from the \emph{subject conversion} property, we know that \(\Gamma\vdash A \convbg B\).

The only thing we need now to apply the \textsc{conv} rule is to show that \(\Gamma\vdash A : s\) for some sort \(s\). However, this is not possible in general, for example when \(A =\tkind\). We have two cases to prove:

\begin{itemize}

\item If \(A = kind\), then using Lemma TODO, we can show that \(B = kind\), hence subject reduction is satisfied

\item If \(A \neq kind\), because \(A\) is inhabited, we can use Lemma TODO to conclude that \(\Gamma\vdash A :s\). Hence we can apply the \textsc{conv}, this closes the proof.