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

\end{definition}

\begin{lemma}[$\tkind$ unicity]

\label{lemma:kindunicity}

For all well-formed context $\Gamma$, if there exists a term $K$ such that $K \convbg\tkind$ and a term $t$ such that $\Gamma\vdash t : K$ then necessarily $K =\tkind$.

\end{lemma}

\begin{proof}

\todo{PROOF}

\end{proof}

\begin{lemma}[$\ttype$-terms are $\tkind$]

Let $\Gamma$ be a well-formed context and $t$, $K$ a terms such that $\Gamma\vdash t : K$ then $\ttype$ is a subterm of $t$ if and only if $K =\tkind$.

\end{lemma}

\begin{proof}

\todo{PROOF}

\end{proof}

\begin{lemma}

When the relation system is oriented (a rewriting system) then

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

...

...

@@ -195,7 +210,7 @@ The subjection conversion property is a generalization of a subject reduction in

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 =\tkind\), then using Lemma~\ref{lemma:kindunicity}, 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}

...

...

@@ -206,28 +221,7 @@ The subjection conversion property is a generalization of a subject reduction in

for all terms $t, A, B$, if $\Gamma\vdash t : A$ and $\Gamma\vdash t : B$

then $A \convbg B$.

\end{lemma}

\begin{lemma}[$\tkind$ unicity - Maybe true]

For all well-formed context $\Gamma$, if there exists a term $K$ such that $K \convbg\tkind$ and a term $t$ such that $\Gamma\vdash t : K$ then necessarily $K =\tkind$.

\end{lemma}

\begin{lemma}[$\ttype$-terms are $\tkind$ - Maybe true]

Let $\Gamma$ be a well-formed context and $t$, $K$ a terms such that $\Gamma\vdash t : K$ then $\ttype$ is a subterm of $t$ if and only if $K =\tkind$.

\end{lemma}

\begin{lemma}[False]

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

\end{lemma}

\begin{lemma}[False]

For any context \(\Gamma\), if \(\ttype\convbg t\) then \(t =\ttype\).