Commit d9a15f57 authored by Gaspard Ferey's avatar Gaspard Ferey

New lemmas.

parent b28e6140
......@@ -75,7 +75,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
{\wf{\Gamma, \mathcal{R}}}
\Gamma \vdash A : s
\Gamma \vdash t : A
......@@ -169,6 +169,7 @@ Note: \(\mathcal{T}_{\mathcal{\emptyset}}\) is the set of closed terms.
Remark: when $T_1$ (resp. $T_2$) is typable with a sort, $\Gamma \vdash T_1 :s$ (resp. $\Gamma \vdash T_2 :s$), then it follows from $T_1 \convbg T_2$ that $\Gamma \vdash t_2 : T_1$ (resp. $\Gamma \vdash t_2 : T_1$).
When the relation system is oriented (a rewriting system) then
\emph{subject conversion} and \emph{typability preservation} together
......@@ -215,6 +216,22 @@ $$
\begin{lemma}[Type convertibility]
For all well-formed context $\Gamma$ satisfying
the \emph{subject conversion} property,
for all terms $t, A, B$, if $\Gamma \vdash t : A$ and $\Gamma \vdash t : B$
then $A \convbg B$.
\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$.
\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$.
For any well-formed context \(\Gamma\), and term $t$ such that \(\tkind \convbg t\) then \(t = \tkind\).
......@@ -231,7 +248,7 @@ $$
we can prove that there is no \(u\) such that \(\Gamma \vdash \wf{(\tkind,u)}\) or the symmetrical case are derivable.
For any context \(\Gamma\), if \(\ttype \convbg t\) then \(t = \ttype\).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment