\documentclass[draft]{article}
\input linear
\def\bad#1{{\em [XXX: #1]}}
\def\cn{{:}}
\def\dv{{\div}}
\def\sr{{\star}}
\def\vv{\mathrel{\vdash\!\!\!\vdash}}
\def\isem{{\mathrel;\mkern-9.5mu\mathrel-}}
\def\ssem{{\mathrel,\mkern-7mu\mathrel\star}}
\def\rnil{{\sans nil}}
\def\rtype{{\sans type}}
\def\rkind{{\sans kind}}
\def\whr{\mathrel{\mathop{\longrightarrow}\limits^{whr}}}
\begin{document}
%\title{LFIN \break
%\small ({\bf LF} with {\bf I}rrelevance and {\bf N}otational definitions)}
\title{LF with Irrelevance and Notational Definitions}
\author{Jason Reed}
\maketitle
\tableofcontents
%
\section{Language}
\begin{center}\begin{tabular}{lll}
Kinds&$K$&$::=\rtype\celse \Pi x \cn A . K \celse \Pi x \dv A . K$\\
Types&$A$&$::=a\cdot S \celse \Pi x \cn A . B \celse \Pi x \dv A . B$\\
Objects&$M$&$::= H \cdot S  \celse \lambda x \cn A . M \celse \lambda x \dv A . M
\celse M \cdot S$\\
Spines&$S$&$::= \rnil \celse (M ; S) \celse (M\ \isem S)$\\
Heads&$H$&$::= c \celse x \celse d$\\
\\
Signatures&$\Sigma$&$::= \cdot \celse \Sigma, a : K\celse \Sigma, c : A
\celse \Sigma, d : A = M$\\
Contexts&$\Gamma$&$::= \cdot \celse \Gamma, x : A \celse \Gamma, x \div A$\\
Erased Contexts&$\Gamma^\square$&$::= \cdot \celse \Gamma^\square, x$\\
\end{tabular}\end{center}
%
\section{Proof Typing}
Functions:
\begin{center}\begin{tabular}{llp{1.8in}}
Proof Promotion&$\Gamma \mapsto \Gamma^\oplus$&
Promote proof variables in $\Gamma$ to term variables\\
\end{tabular}\end{center}
Judgments:
\begin{center}\begin{tabular}{llp{1.8in}}
Proof Object Typing&$\Gamma \prov M \div A$&
In $\Gamma$, $M$ has irrelevant type $A$.\\
\end{tabular}\end{center}
%
\subsection{Proof Promotion}
\begin{eqnarray*}
\cdot^\oplus &:=& \cdot\\
(\Gamma, x : A)^\oplus &:=& \Gamma^\oplus, x : A\\
(\Gamma, x \div A)^\oplus &:=& \Gamma^\oplus, x : A
\end{eqnarray*}
%
\subsection{Proof Object Typing}
$$\begin{prooftree}
\Gamma^\oplus \prov M : A \qquad \Gamma \prov A : \rtype
\using \ir pot. \justifies
\Gamma \prov M \div A
\end{prooftree}$$
%
\section{Typing}
Judgments:
\begin{center}\begin{tabular}{llp{1.8in}}
Spine Typing&$\Gamma \prov S : A > a$&
In $\Gamma$, $S$ gives base type $a$ for a head of type $A$.\\
Type Spine Kinding&$\Gamma \prov S : K \gg \rtype$&
In $\Gamma$, $S$ gives a type for a head of kind $K$.\\
Object Typing&$\Gamma \prov M : A$&
In $\Gamma$, $M$ has type $A$.\\
Type Validity&$\Gamma \prov A : \rtype$&
In $\Gamma$, $A$ is a valid type.\\
Kind Validity&$\Gamma \prov K : \rkind$&
In $\Gamma$, $K$ is a valid kind.\\
\end{tabular}\end{center}
%
\subsection{Spine Typing}
$$\begin{prooftree}
\using \ir st_nil. \justifies
\Gamma \prov \rnil : A > A
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M : A \qquad \Gamma \prov S : [M/x] B > C
\using \ir st_cons. \justifies
\Gamma \prov (M ; S) : \Pi x \cn A . B > C
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M \div A \qquad \Gamma \prov S : [M/x] B > C
\using \ir st_icons. \justifies
\Gamma \prov (M\ \isem S) : \Pi x {\div} A . B > C
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov S : A > B \qquad \Gamma \prov B = B' : \rtype
\using \ir st_conv. \justifies
\Gamma \prov S : A > B'
\end{prooftree}$$
%
\subsection{Type Spine Kinding}
$$\begin{prooftree}
\using \ir tsk_nil. \justifies
\Gamma \prov \rnil : \rtype \gg \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M : A \qquad \Gamma \prov S : [M/x] K \gg \rtype
\using \ir tsk_cons. \justifies
\Gamma \prov (M ; S) : \Pi x \cn A . K \gg \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M \div A \qquad \Gamma \prov S : [M/x] K \gg \rtype
\using \ir tsk_icons. \justifies
\Gamma \prov (M\ \isem S) : \Pi x {\div} A . K \gg \rtype
\end{prooftree}$$
%
\subsection{Object Typing}
$$\begin{prooftree}
c : A \in \Sigma \qquad \Gamma \prov S : A > B
\using \ir ot_const. \justifies
\Gamma \prov c \cdot S : B
\end{prooftree}$$
$$\begin{prooftree}
x : A \in \Gamma \qquad \Gamma \prov S : A > B
\using \ir ot_var. \justifies
\Gamma \prov x \cdot S : B 
\end{prooftree}$$
$$\begin{prooftree}
d : A = M \in \Sigma \qquad \Gamma \prov S : A > B
\using \ir ot_def. \justifies
\Gamma \prov d \cdot S : B 
\end{prooftree}$$
$$\begin{prooftree}
\Gamma, x\star A \prov M : B \qquad \Gamma \prov A : \rtype
\using \ir ot_lam. \justifies
\Gamma \prov \lambda x\sr A . M : \Pi x \sr A . B
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M : A \qquad \Gamma \prov S : A > B
\using \ir ot_app. \justifies
\Gamma \prov M \cdot S : B
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M : A \qquad \Gamma \prov A = B : \rtype
\using \ir ot_conv. \justifies
\Gamma \prov M : B
\end{prooftree}$$
%
\subsection{Type Validity}
$$\begin{prooftree}
a : K \in \Sigma \qquad \qquad \Gamma \prov S : K \gg \rtype
\using \ir tv_const. \justifies
\Gamma \prov a \cdot S : \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov A : \rtype \qquad \Gamma, x \star A \prov B : \rtype
\using \ir tv_pi. \justifies
\Gamma \prov \Pi x \sr A . B :  \rtype
\end{prooftree}$$
%
\subsection{Kind Validity}
$$\begin{prooftree}
\using \ir kv_type. \justifies
\Gamma \prov \rtype : \rkind
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov A : \rtype \qquad \Gamma, x \star A \prov K : \rkind
\using \ir kv_pi. \justifies
\Gamma \prov \Pi x \sr A . K :  \rkind
\end{prooftree}$$
%
\section{Equality}
Judgments:
\begin{center}\begin{tabular}{p{1.0in}lp{1.8in}}
Proof Equality&$\Gamma \prov M_1 = M_2 \div A$&
In $\Gamma$, $M_1=M_2$ at irrelevant type $A$.\\
Object Equality&$\Gamma \prov M_1 = M_2 : A$&
In $\Gamma$, $M_1=M_2$ at type $A$.\\
Type Equality&$\Gamma \prov A_1 = A_2 : \rtype$&
In $\Gamma$, $A_1$ and $A_2$ are equal types.\\
Kind Equality&$\Gamma \prov K_1 = K_2 : \rkind$&
In $\Gamma$, $K_1$ and $K_2$ are equal kinds.\\
Spine Equality&$\Gamma \prov S_1 = S_2 : A>B$&
In $\Gamma$, $S_1=S_2$ at type $A>B$.\\
Type Spine\hfil\break Equality&$\Gamma \prov S_1 = S_2 : K \gg \rtype$&
In $\Gamma$, $S_1=S_2$ at kind $\rtype$.
\end{tabular}\end{center}
%
\subsection{Proof Equality}
$$\begin{prooftree}
\Gamma^\oplus \prov M = M : A \qquad \Gamma^\oplus \prov N = N : A \qquad \Gamma \prov A : \rtype
\using \ir pe. \justifies
\Gamma\prov M = N \div A
\end{prooftree}$$
%
\subsection{Object Equality}
\subsubsection{Simultaneous Congruence}
$$\begin{prooftree}
c : A \in \Sigma \qquad \Gamma \prov S_1 = S_2 : A > B
\using \ir oe_const. \justifies
\Gamma \prov c \cdot S_1 = c \cdot S_2 : B
\end{prooftree}$$
$$\begin{prooftree}
x : A \in \Gamma \qquad \Gamma \prov S_1 = S_2 : A > B
\using \ir oe_var. \justifies
\Gamma \prov x \cdot S_1 = x \cdot S_2 : B
\end{prooftree}$$
$$\begin{prooftree}
d : A = M \in \Sigma \qquad \Gamma \prov M \cdot S_1 = M \cdot S_2 : B
\using \ir oe_def. \justifies
\Gamma \prov d \cdot S_1 = d \cdot S_2 : B
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov  A_1' = A_1 : \rtype \qquad
\Gamma \prov  A_1'' = A_1 : \rtype \qquad
\Gamma, x \star A_1 \prov  M = N : A_2
\using \ir oe_lam. \justifies
\Gamma \prov \lambda x \sr A_1' . M = \lambda x \sr A_1'' . N : \Pi x \sr A_1 . A_2
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov  M_1 = M_2 : A \qquad
\Gamma \prov  S_1 = S_2 : A > B 
\using \ir oe_app. \justifies
\Gamma \prov M_1 \cdot S_1 = M_2 \cdot S_2 : B
\end{prooftree}$$
\subsubsection{Extensionality}
$$\begin{prooftree}
\Gamma \prov A_1 : \rtype \qquad
{\{\Gamma \prov M_1, M_2 : \Pi x \cn A_1 . A_2\}
\atop \Gamma, x : A_1 \prov M_1 \cdot (x \cdot \rnil; \rnil) = M_2 \cdot (x \cdot \rnil; \rnil) : A_2}
\using \ir oe_ext. \justifies
\Gamma \prov M_1 = M_2 : \Pi x \cn A_1 . A_2
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov A_1 : \rtype \qquad
{\{\Gamma \prov M_1, M_2 : \Pi x \dv A_1 . A_2\}
\atop \Gamma, x \div A_1 \prov M_1 \cdot (x \cdot \rnil\ \isem \rnil) = M_2 \cdot (x \cdot \rnil\ \isem \rnil) : A_2}
\using \ir oe_iext. \justifies
\Gamma \prov M_1 = M_2 : \Pi x \dv A_1 . A_2
\end{prooftree}$$
\subsubsection{Parallel Reduction}
$$\begin{prooftree}
\Gamma \prov M = N : B
\using \ir oe_red_nil. \justifies
\Gamma \prov M \cdot \rnil = N : B
\end{prooftree}$$
$$\begin{prooftree}
\Gamma\prov H \cdot \rnil : B \qquad \Gamma \prov S_1 = S_2 : B > C
\using \ir oe_red_nil2. \justifies
\Gamma \prov (H  \cdot \rnil) \cdot S_1 = H \cdot S_2 : C
\end{prooftree}$$

$$\begin{prooftree}
\[\Gamma, x : B \prov M_1 = M_2 : A \djust \Gamma \prov N_1 = N_2 : B\]
\qquad \Gamma, x : B \prov S = S' : A > C
\using \ir oe_red_cons.\justifies
\Gamma \prov (\lambda x \cn B . M_1) \cdot (N_1 ; S) = [N_2/x]M_2 \cdot S' : [N_1/x]C
\end{prooftree}$$
$$\begin{prooftree}
\[\Gamma, x \div B \prov M_1 = M_2 : A \djust \Gamma \prov N_1 = N_2 \div B\]
\qquad \Gamma, x \div B \prov S = S' : A > C
\using \ir oe_red_icons.\justifies
\Gamma \prov (\lambda x \dv B . M_1) \cdot (N_1\ \isem S) = [N_2/x]M_2 \cdot S' : [N_1/x]C
\end{prooftree}$$
\subsubsection{Type Conversion}
$$\begin{prooftree}
\Gamma \prov M = N : A \qquad \Gamma \prov A = B : \rtype
\using \ir oe_conv. \justifies
\Gamma \prov M = N : B
\end{prooftree}$$
%
\subsection{Type Equality}
\subsubsection{Simultaneous Congruence}
$$\begin{prooftree}
a : K \in \Sigma \qquad \Gamma \prov S_1 = S_2 : K \gg \rtype
\using \ir te_const. \justifies
\Gamma \prov a \cdot S_1 = a \cdot S_2 : \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov  A' = A : \rtype \qquad
\Gamma, x \star A \prov  B = B' : \rtype
\using \ir te_pi. \justifies
\Gamma \prov \Pi x \sr A . B = \Pi x \sr A' . B' : \rtype
\end{prooftree}$$
%
\subsection{Kind Equality}
\subsubsection{Simultaneous Congruence}
$$\begin{prooftree}
\using \ir ke_type. \justifies
\Gamma \prov \rtype = \rtype : \rkind
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov  A' = A : \rtype \qquad
\Gamma, x \star A \prov  K = K' : \rkind
\using \ir ke_pi. \justifies
\Gamma \prov \Pi x \sr A . K = \Pi x \sr A' . K' : \rkind
\end{prooftree}$$
%

\subsection{Spine Equality}
\subsubsection{Simultaneous Congruence}
$$\begin{prooftree}
\using \ir se_nil. \justifies
\Gamma \prov \rnil = \rnil : A > A
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M_1 = M_2 : A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]B > C
\using \ir se_cons. \justifies
\Gamma \prov (M_1 ; S_1) = (M_2 ; S_2) : \Pi x \cn A . B > C
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M_1 = M_2 \div A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]B > C
\using \ir se_icons. \justifies
\Gamma \prov (M_1\ \isem S_1) = (M_2\ \isem S_2) : \Pi x \dv A . B > C
\end{prooftree}$$
%
\subsection{Type Spine Equality}
\subsubsection{Simultaneous Congruence}
$$\begin{prooftree}
\using \ir tse_nil. \justifies
\Gamma \prov \rnil = \rnil : \rtype \gg \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M_1 = M_2 : A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]K \gg \rtype
\using \ir tse_cons. \justifies
\Gamma \prov (M_1 ; S_1) = (M_2 ; S_2) : \Pi x \cn A . K \gg \rtype
\end{prooftree}$$
$$\begin{prooftree}
\Gamma \prov M_1 = M_2 \div A \qquad \Gamma \prov S_1 = S_2 : [M_1/x]K \gg \rtype
\using \ir tse_icons. \justifies
\Gamma \prov (M_1\ \isem S_1) = (M_2\ \isem S_2) : \Pi x \dv A . K \gg \rtype
\end{prooftree}$$
%%%
\begin{lemma}[Functionality]
\begin{enumerate}

\end{enumerate}
\end{lemma}
\begin{proof}

\cqed
\end{proof}
\begin{lemma} ($\eta$-conversion)
\label{eta}
\begin{enumerate}
\item If $\Gamma \prov M : \Pi x \cn A . B$, then $\Gamma \prov M = \lambda x \cn A . M \cdot (x \cdot \rnil ; \rnil) : \Pi x \cn A . B$
\item If $\Gamma \prov M : \Pi x \dv A . B$, then $\Gamma \prov M = \lambda x \dv A . M \cdot (x \cdot \rnil\ \isem \rnil) : \Pi x \dv A . B$
\end{enumerate}
\end{lemma}
\begin{proof}\ 
\begin{enumerate}
\item
{\small
$$\begin{prooftree}
\[
\[\using \ir oe_red_nil. \justifies x \cdot \rnil = (x \cdot \rnil) \cdot \rnil \]\[\justifies (x\cdot \rnil ; \rnil) = (x\cdot \rnil ; \rnil)\]
\using \ir oe_red_cons. \justifies
\Gamma, x : A \prov M \cdot (x \cdot \rnil ; \rnil) = (\lambda y \cn A . M \cdot (y \cdot \rnil ; \rnil)) \cdot (x \cdot \rnil ; \rnil) :  B
\]
\using \ir oe_ext.\justifies
\Gamma \prov M = \lambda y \cn A . M \cdot (y \cdot \rnil ; \rnil) : \Pi y \cn A . B
\end{prooftree}$$}
\item Similar.
\end{enumerate}
\cqed
\end{proof}
%%%
\begin{lemma} (Spine Splicing)
\label{splice}
\begin{enumerate}
\item If $\Gamma \prov S : A > B$, $\Gamma \prov M : \Pi x \cn C . A$ and $\Gamma \prov N : C$,
then $\Gamma\prov M \cdot (N; S) = (M \cdot (N; \rnil)) \cdot S : B$
\item If $\Gamma \prov S : A > B$, $\Gamma \prov M : \Pi x \dv C . A$ and $\Gamma \prov N \div C$,
then $\Gamma\prov M \cdot (N\ \isem S) = (M \cdot (N\ \isem \rnil)) \cdot S : B$
\end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}
\item By Lemma~\ref{eta} and $\ir oe_app.$, we know
$$\Gamma \prov M \cdot (N; S) = (\lambda x \cn A . M \cdot (x \cdot \rnil ; \rnil)) \cdot (N ; S) : B$$
By $\ir oe_red_cons.$, (using $\ir oe_red_nil.$ to see that $N \cdot \rnil = N$) we have 
$$\Gamma \prov M \cdot (N; S) =  (M \cdot (N; \rnil)) \cdot S : B$$
as required.
\item Similar.
\end{enumerate}
\cqed
\end{proof}

\begin{lemma} (Validity)
\begin{enumerate}
\item If $\Gamma\prov M \star A$, then $\Gamma \prov A : \rtype$.
\item If $\Gamma\prov S : A > B$ and $\Gamma \prov A : \rtype$, then $\Gamma \prov B : \rtype$.
\item If $\Gamma, x \star A\prov B : \rtype$ and $\Gamma \prov M \star A$, then $\Gamma \prov [M/x]B : \rtype$.
\item If $\Gamma\prov M_1 = M_2 \star A$, then $\Gamma \prov M_1 \star A$ and $\Gamma \prov M_2 \star A$.
\item If $\Gamma\prov S_1 = S_2 : A > B$, then $\Gamma \prov S_1 : A > B$ and $\Gamma \prov S_2 : A > B$.
\item If $\Gamma\prov A_1 = A_2 : \rtype$, then $\Gamma \prov A_1 : \rtype$ and $\Gamma \prov A_2 : \rtype$.
\end{enumerate}
\end{lemma}
\begin{proof}
By induction on the appropriate rules.
\cqed
\end{proof}
\begin{lemma} (Unicity)
\begin{enumerate}
\item If $\Gamma\prov M \star A$ and $\Gamma\prov M \star A'$, then $\Gamma \prov A = A' : \rtype$.
\item If $\Gamma\prov S : A > B$, and $\Gamma \prov S : A' > B'$, and also $\Gamma \prov A = A' : \rtype$,
then $\Gamma \prov B = B' : \rtype$.
\end{enumerate}
\end{lemma}
\begin{proof}
By simultaneous induction on the structure of the relevant typing deductions.
\cqed
\end{proof}
%\begin{lemma}
%If $\Gamma \prov S : A > B$, then $B$ is of the form $a \cdot S'$.
%\end{lemma}
%\begin{proof}
%By induction on the spine typing and type equality rules.
%\cqed
%\end{proof}
%\begin{lemma} (Extensionality)
%%If $\Gamma \prov M : \Pi x_1 : A_1 . \Pi x_2 : A_2 . \cdots  \Pi x_n : A_n . B$, then
%%$M$ is of the form $\lambda x_1 : A_1 . \lambda x_2 . A_2 . \cdots \lambda x_n : A_n . M'$,
%%and $\Gamma, x_1 : A_1, x_2 : A_2, \ldots, x_n : A_n \prov M' : B$.
%If $\Gamma \prov M : \Pi x \sr A . B$, then
%$M$ is of the form $\lambda x \sr A . M'$,
%and $\Gamma, x \star A \prov M' : B$.
%\end{lemma}
%\begin{proof}
%By induction on the object typing and type equality rules. 
%\cqed
%\end{proof}
%
\section{Strictness}
\def\rpat{{\ \sans pat}}
Functions:
\begin{center}\begin{tabular}{llp{1.8in}}
Erasure&$\Gamma \mapsto \Gamma^\square$&
Remove types and irrelevant variables from $\Gamma$\\
\end{tabular}\end{center}
Judgments:
\begin{center}\begin{tabular}{llp{1.8in}}
Pattern Spine&$\Delta^\square \prov S \rpat$&
In $\Delta$, $S$ is a pattern spine.\\
Local Strict Occurrences&$\Gamma;\Delta \vv_x M$&
$x$ occurs locally strict in $M$\\
&$\Gamma;\Delta \vv_x A$&
$x$ occurs locally strict in $A$\\
&$\Gamma;\Delta \vv_x S$&
$x$ occurs locally strict in $S$\\
Strict Occurrences&$\Gamma \vv_x M$&
$x$ occurs strict in $M$\\
Strictness&$\Gamma \vv M$&
$M$ is strict\\
\end{tabular}\end{center}
%
\subsection{Erasure}
\begin{eqnarray*}
\cdot^\square &:=& \cdot\\
(\Gamma, x : A)^\square &:=& \Gamma^\square, x^: \\
(\Gamma, x \div A)^\square &:=& \Gamma^\square, x^\div
\end{eqnarray*}
\subsection{Pattern Spines}
$$\begin{prooftree}
\using \ir pat_nil. \justifies
\Delta^\square \prov \rnil \rpat
\end{prooftree}$$
$$\begin{prooftree}
\Delta^\square \prov S \rpat \qquad x^\star \not\in \Delta^\square
\using \ir pat_cons. \justifies
\Delta^\square, x^: \prov (x; S) \rpat
\end{prooftree}$$
$$\begin{prooftree}
\Delta^\square \prov S \rpat 
\using \ir pat_icons. \justifies
\Delta^\square \prov (M\ \isem S) \rpat
\end{prooftree}$$
%%%
\begin{lemma}
Suppose $\Gamma \prov N_1, N_2 \div A$.
\begin{enumerate}
\item If $\Gamma, z \div A \prov M \star B$, then $\Gamma \prov [N_1/z]M = [N_2/z]M \star [N_1/z]B$.
\item If $\Gamma, z \div A \prov S : A > B$, then $\Gamma \prov [N_1/z]S = [N_2/z]S : [N_1/z]A > [N_1/z]B$.
\item If $\Gamma, z \div A \prov B \star \rtype$, then $\Gamma \prov [N_1/z]B = [N_2/z]B \star \rtype$.
\end{enumerate}
\label{irrel.subst}
\end{lemma}
\begin{proof}
Simultaneous induction on the object and spine typing and type validity rules.
\cqed
\end{proof}
%%%
\begin{lemma}\label{nil.replace}\ 
\begin{enumerate} 
\item If $\Gamma \prov M : A$, then $\Gamma \prov [x\cdot \rnil / x]M =  M : A$.
\item If $\Gamma \prov S : A > B$, then $\Gamma \prov [x\cdot \rnil / x]S =  S : A > B$.
\item If $\Gamma \prov A : \rtype$, then $\Gamma \prov [x\cdot \rnil / x]A =  A : \rtype$.
\end{enumerate}
\end{lemma}
\begin{proof}
Simultaneous induction on the object and spine typing and type validity rules.
The critical case is $\ir ot_var.$, where we use $\ir oe_red_nil2.$.
\cqed
\end{proof}
%%%
\begin{lemma}\label{pi.nil.replace}
If $\Gamma \prov \Pi y \sr B . B' : \rtype$ and $x \not \in \Gamma$, then
$\Gamma \prov \Pi x \sr B. [x\cdot \rnil / y] B' = \Pi y \sr B . B' : \rtype$.
\end{lemma}
\begin{proof}
By $\alpha$-conversion, we know $\Gamma \prov \Pi x \sr B . [x/y]B' : \rtype$,
and inversion on the type validity rules gives
$\Gamma, x \star B \prov  [x/y]B' : \rtype$.
By Lemma~\ref{nil.replace} and the fact that $x\not\in\Gamma$ and consequently $x$ does not appear free in $B'$,
we know $\Gamma, x \star B \prov [x\cdot \rnil / y]B' : \rtype$,
hence $\Gamma \prov \Pi x \sr B . [x\cdot \rnil / y]B' : \rtype$, as required.
\cqed
\end{proof}
%%%
\begin{lemma}
If 
\begin{enumerate}
\item $\Delta^\square \prov S \rpat$,
\item $\Gamma \prov M_1, M_2 : A_2$,
\item $\Delta \prov S : A_1 > C$,
\item $\Gamma, \Delta \prov A_1 = A_2 : \rtype$
\item $\Gamma, \Delta \prov M_1 \cdot S = M_2 \cdot S : C$, and \label{big.assume}
\item The variable names in $\Gamma$ and $\Delta$ are disjoint.
\end{enumerate}
then $\Gamma \prov M_1 = M_2 : A_2$.
\end{lemma}
\begin{proof}
By induction on $\D :: \Delta^\square \prov S \rpat$.
\begin{itemize}
\item[Case:]
$$\D = \begin{prooftree}
\using \ir pat_nil. \justifies
\Delta^\square \prov \rnil \rpat
\end{prooftree}$$
In this case, $S = \rnil$. By inversion on the spine typing rules, $A_1$ is identical to $C$,
so we have $\Gamma, \Delta \prov C = A_2 : \rtype$.
We know that $\Gamma, \Delta \prov M_1 \cdot \rnil = M_2 \cdot \rnil : C$,
so by $\ir oe_red_nil.$ we can conclude $\Gamma, \Delta \prov M_1 = M_2 : C$. By $\ir oe_conv.$, we know
$\Gamma, \Delta \prov M_1 = M_2 : A_2$. But no variable from $\Delta$ appears free in $M_1$ or $M_2$,
so $\Gamma \prov M_1 = M_2 : A_2$.
\item[Case:]
$$\D = \begin{prooftree}
\[ \D' \djust (\Delta')^\square \prov S' \rpat \] \[ \djust x^\star \not\in (\Delta')^\square \]
\using \ir pat_cons. \justifies
(\Delta')^\square, x^: \prov (x \cdot \rnil; S') \rpat
\end{prooftree}$$
In this case, $S = (x \cdot \rnil; S')$ and $x : B \in \Delta$ for some $B : \rtype$.
So we know $\Delta \prov (x \cdot \rnil ; S') : A_1 > C$.
Assumption~(\ref{big.assume}) in this case is
$$\Gamma, \Delta \prov M_1 \cdot (x \cdot \rnil; S') = M_2 \cdot (x \cdot \rnil; S') : C$$
By Lemma~\ref{splice} we can infer
$$\Gamma, \Delta \prov (M_1 \cdot (x \cdot \rnil; \rnil)) \cdot S' = (M_2 \cdot (x \cdot \rnil;\rnil)) \cdot S' : C$$
Now by inversion on the spine typing rules, $A_1$ must be of the form $\Pi y \cn B . B'$, such
that $\Delta' \prov S' : [x\cdot\rnil/y]B' > C$.
Notice that we can also now show that
$$\Gamma, x : B \prov M_1 \cdot (x \cdot \rnil; \rnil), M_2 \cdot (x \cdot \rnil; \rnil) : [x\cdot\rnil/y]B'$$
and $\Gamma, \Delta \prov B' = B' : \rtype$, and also $\Gamma, x : B$ is
disjoint from $\Delta'$.
By the induction hypothesis, we get
$$\Gamma, x : B \prov (M_1 \cdot (x \cdot \rnil; \rnil)) = (M_2 \cdot (x \cdot \rnil;\rnil)) : [x\cdot\rnil/y]B'$$
Using $\ir oe_ext.$, and Lemma~\ref{pi.nil.replace}, we conclude
$$\Gamma, \Delta \prov M_1 = M_2 : \Pi y \cn B . B'$$
and so
$$\Gamma \prov M_1 = M_2 : A_2$$ by type conversion and the observation that no variables in $\Delta$
appear free in $M_1$ or $M_2$ by their typing.
\item[Case:]
$$\D = \begin{prooftree}
\[ \D' \djust \Delta^\square \prov S' \rpat \] 
\using \ir pat_icons. \justifies
\Delta^\square \prov (M'\ \isem S') \rpat
\end{prooftree}$$
In this case, $S = (M' \ \isem S')$. 
By inversion on the spine typing rules, $\Delta \prov M'  \div B$ for some $B \div \rtype$
and $A_1$ is of the form $\Pi y \dv B . B'$, such that $\Delta \prov S' : [M'/y]B' > C$.
So we know $\Delta \prov (M' \ \isem S') : \Pi y \dv B . B'  > C$.
Assumption~(\ref{big.assume}) in this case is
$$\Gamma, \Delta \prov M_1 \cdot (M' \ \isem S') = M_2 \cdot (M' \ \isem S') : C$$
By Lemma~\ref{splice} we can infer
$$\Gamma, \Delta \prov (M_1 \cdot (M' \ \isem \rnil)) \cdot S' = (M_2 \cdot (M' \ \isem\rnil)) \cdot S' : C$$
Now create a fresh variable $\bar x : A$ for each $x : A\in \Delta$. Put $\bar\Delta = \{\bar x : A \st x : A \in \Delta\}$.
We have (by the triviality of equality at irrelevant type) that
$$\Delta,\bar \Delta \prov M' = [\bar\Delta / \Delta]M' \div B$$
and so
$$\Gamma, \bar\Delta, \Delta \prov (M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil)) \cdot S' = (M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem\rnil)) \cdot S' : C$$
by using Lemma~\ref{irrel.subst}.
Notice that we do not substitute for any occurrences of $M'$ in $S'$.
We can also now show that
$$\Gamma, \bar \Delta \prov M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil), M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil) : [[\bar\Delta/\Delta]M'/y]B'$$
and $\Gamma, \bar\Delta, \Delta \prov [M'/y]B' = [[\bar\Delta/\Delta]M'/y]B' \div \rtype$, and also $\Gamma, \bar\Delta$ is
disjoint from $\Delta$, since the variables in $\bar\Delta$ were chosen to be fresh.
By the induction hypothesis, we get
$$\Gamma, \bar \Delta \prov (M_1 \cdot ([\bar\Delta/\Delta]M' \ \isem \rnil)) = (M_2 \cdot ([\bar\Delta/\Delta]M' \ \isem\rnil)) : [[\bar\Delta/\Delta]M'/y]B'$$
Using Lemma~\ref{irrel.subst} again, we can see that
$$\Gamma, \bar \Delta, w \div [\bar\Delta/\Delta]B \prov (M_1 \cdot (w \cdot \rnil \ \isem \rnil)) = (M_2 \cdot (w\cdot \rnil\ \isem\rnil)) : [w\cdot \rnil/y]B'$$
By, $\ir oe_ext.$
$$\Gamma, \bar \Delta \prov M_1  = M_2 : \Pi w \dv [\bar\Delta/\Delta]B . [w\cdot \rnil/y]B'$$
Lemma~\ref{pi.nil.replace} provides the simplification
$$\Gamma, \bar \Delta \prov M_1  = M_2 : \Pi w \dv [\bar\Delta/\Delta]B . [w/y]B'$$
and $\alpha$-conversion gives
$$\Gamma, \bar \Delta \prov M_1  = M_2 : \Pi y \dv [\bar\Delta/\Delta]B . B'$$
But we can kind convert to
$$\Gamma, \bar \Delta, \Delta \prov M_1 = M_2 : \Pi y \dv B . B'$$
and so
$$\Gamma \prov M_1 = M_2 : A_2$$ by strengthening, using the observation that no variables in $\Delta,\bar \Delta$
can appear free in $M_1$ or $M_2$ by their typing.
\end{itemize}
\cqed
\end{proof}
\subsection{Local Strict Occurrences}
$$\begin{prooftree}
\Delta \prov S \rpat \qquad \Delta \prov S : B > C
\using \ir ls_pat. \justifies
\Gamma;\Delta \vv_x x \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\Gamma ; \Delta \vv_x M
\using \ir ls_hd. \justifies
\Gamma ; \Delta \vv_x (M ; S)
\end{prooftree}
\qquad%%%%%%%%%%%%%%
\begin{prooftree}
\Gamma ; \Delta \vv_x S
\using \ir ls_sp. \justifies
\Gamma ; \Delta \vv_x (M ; S)
\end{prooftree}$$
$$\begin{prooftree}
\Gamma ; \Delta \vv_x S
\using \ir ls_isp. \justifies
\Gamma ; \Delta \vv_x (M\ \isem S)
\end{prooftree}$$
$$\begin{prooftree}
y : A \in \Delta \qquad \Gamma ; \Delta \vv_x S
\using \ir ls_var. \justifies
\Gamma ; \Delta \vv_x y \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\Gamma ; \Delta \vv_x S
\using \ir ls_a. \justifies
\Gamma ; \Delta \vv_x a \cdot S
\end{prooftree}
\qquad%%%%%%%%%%%%%%
\begin{prooftree}
\Gamma ; \Delta \vv_x S
\using \ir ls_c. \justifies
\Gamma ; \Delta \vv_x c \cdot S
\end{prooftree}$$
$$\begin{prooftree}
d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma ; \Delta \vv_x S
\using \ir ls_d. \justifies
\Gamma ; \Delta \vv_x d \cdot S
\end{prooftree}$$
$$\begin{prooftree}
M \whr M' \qquad \Gamma; \Delta\vv_x M'
\using \ir ls_red. \justifies
\Gamma ; \Delta \vv_x M
\end{prooftree}$$
$$\begin{prooftree}
\Gamma; \Delta \vv_x A
\using \ir ls_ld. \justifies
\Gamma; \Delta \vv_x \lambda y : A . M
\end{prooftree}
\qquad%%%%%%%%%%%%%%
\begin{prooftree}
\Gamma; \Delta, y \star A \vv_x M
\using \ir ls_lb. \justifies
\Gamma; \Delta \vv_x \lambda y \star A . M
\end{prooftree}$$
$$\begin{prooftree}
\Gamma; \Delta \vv_x A_1
\using \ir ls_pd. \justifies
\Gamma; \Delta \vv_x \Pi y : A_1 . A_2
\end{prooftree}
\qquad%%%%%%%%%%%%%%
\begin{prooftree}
\Gamma; \Delta, y \star A_1 \vv_x A_2
\using \ir ls_pb. \justifies
\Gamma; \Delta \vv_x \Pi y \star A_1 . A_2
\end{prooftree}$$
%
\subsection{Strict Occurrences}
$$\begin{prooftree}
M \whr M' \qquad \Gamma \vv_x M'
\using \ir rs_red. \justifies
\Gamma \vv_x M
\end{prooftree}$$
$$\begin{prooftree}
d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma ;  \cdot \vv_x S
\using \ir rs_d. \justifies
\Gamma \vv_x d \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\Gamma ; \cdot \vv_x S
\using \ir rs_c. \justifies
\Gamma  \vv_x c \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\Gamma, y \star A \vv_x M
\using \ir rs_lam. \justifies
\Gamma \vv_x \lambda y \star A . M
\end{prooftree}$$
%
\subsection{Strictness}
$$\begin{prooftree}
M \whr M' \qquad \Gamma \vv M'
\using \ir gs_red. \justifies
\Gamma \vv M
\end{prooftree}$$
$$\begin{prooftree}
d = M : A \in \Sigma \qquad \cdot \vv M \qquad \Gamma \vv M \cdot S
\using \ir gs_d. \justifies
\Gamma \vv d \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\using \ir gs_c. \justifies
\Gamma  \vv c \cdot S
\end{prooftree}$$
$$\begin{prooftree}
\Gamma, x : A \vv_x M \qquad \Gamma, x : A \vv M
\using \ir gs_lam. \justifies
\Gamma \vv \lambda x : A . M
\end{prooftree}$$
$$\begin{prooftree}
\Gamma, x \div A \vv M
\using \ir gs_ilam. \justifies
\Gamma \vv \lambda x \div A . M
\end{prooftree}$$

\begin{lemma}(Completeness)\label{completeness}
Let $\sigma_1, \sigma_2$ be such that $\Gamma'; \Delta' \prov \sigma_1, \sigma_2 : \Gamma; \Delta$.
\begin{enumerate}
\item If 
\begin{enumerate}
\item $x : A\in \Gamma$
\item $\Gamma; \Delta \vv_x M$ 
\item $\Gamma, \Delta \prov M : B$
\item $\Gamma', \Delta' \prov M[\sigma_1] = M[\sigma_2] : B[\sigma_1]$
\end{enumerate}
then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$.
\item If 
\begin{enumerate}
\item $x : A\in \Gamma$
\item $\Gamma; \Delta \vv_x B$ 
\item $\Gamma, \Delta \prov B : \rtype$
\item $\Gamma', \Delta' \prov B[\sigma_1] = B[\sigma_2] : \rtype$
\end{enumerate}
then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$.
\item If 
\begin{enumerate}
\item $x : A\in \Gamma$
\item $\Gamma; \Delta \vv_x S$ 
\item $\Gamma, \Delta \prov S : B > C$
\item $\Gamma', \Delta' \prov S[\sigma_1] = S[\sigma_2] : B[\sigma_1] > C[\sigma_1]$
\end{enumerate}
then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$.
\item If 
\begin{enumerate}
\item $x : A\in \Gamma$
\item $\Gamma \vv_x M$
\item $\Gamma, \Delta\prov M : B$
\item $\Gamma', \Delta' \prov S : B[\sigma_1] > C[\sigma_1]$,
\item $\Gamma' \prov M[\sigma_1] \cdot S = M[\sigma_2] \cdot S : C[\sigma_1]$
\end{enumerate}
then $\Gamma'\prov \sigma_1(x) = \sigma_2(x) : A[\sigma_1]$.
\item If \label{completeness.final}
\begin{enumerate}
\item $\Gamma \vv M$ 
\item $\Gamma \prov M : B$
\item $\Gamma \prov S_1, S_2 : B[\sigma_1] > C[\sigma_1]$
\item $\Gamma' \prov M[\sigma_1] \cdot S_1 = M[\sigma_2] \cdot S_2 : C[\sigma_1]$ 
\end{enumerate}
then $\Gamma'\prov S_1 = S_2 : B[\sigma_1] > C[\sigma_1]$.
\end{enumerate}
\end{lemma}
\begin{proof}
Simultaneous induction over the rules defining the $\vv$ judgments.
\cqed
\end{proof}
\begin{theorem}(Injectivity)
If $d : A = M$ is strict, i.e. $\cdot \vv M$, then $d$ is injective. (as in \cite{strictness})
\end{theorem}
\begin{proof}
Follows immediately from Lemma~\ref{completeness}~(\ref{completeness.final}),
with $\sigma_1,\sigma_2$ both the identity substitution.
\cqed
\end{proof}

\bibliographystyle{alpha}
\bibliography{id}
\end{document}

$$\begin{prooftree}
\Delta^\square \prov S \rpat 
\using \ir pat_iic. \justifies
\Delta^\square, x \div \square \prov (x\  \isem S) \rpat
\end{prooftree}
\qquad
\begin{prooftree}
\Delta^\square, x \div \square \prov S \rpat
\using \ir pat_iic2. \justifies
\Delta^\square, x \div \square \prov (x\  \isem S) \rpat
\end{prooftree}$$
$$\begin{prooftree}
\Delta^\square \prov S \rpat 
\using \ir pat_c. \justifies
\Delta^\square, x : \square \prov (x; S) \rpat
\end{prooftree}$$
$$\begin{prooftree}
\Delta^\square \prov S \rpat 
\using \ir pat_ic. \justifies
\Delta^\square, x : \square \prov (x\ \isem S) \rpat
\end{prooftree}
\qquad
\begin{prooftree}
\Delta^\square, x : \square \prov S \rpat 
\using \ir pat_ic2. \justifies
\Delta^\square, x : \square \prov (x\ \isem S) \rpat
\end{prooftree}$$

$$\Gamma, x \div A', x'\div A' \prov  [x/z][x'/x]M_1' = [x/z][x'/x]M_2' : [x/z]B'$$
and, knowing that there are no free occurrences of $x$ in $[x'/x]M_1'$ or $[x'/x]M_2'$,
we can infer
$$\Gamma, x'\div A' \prov  \lambda x\dv A' . [x/z][x'/x]M_1' = \lambda x \dv A' . [x/z][x'/x]M_2'$$
$$\qquad : \Pi x \dv A' . [x/z][x'/x]B'$$
and then $\alpha$-convert to
$$\Gamma, x'\div A' \prov  \lambda z\dv A' . [x'/x]M_1' = \lambda z \dv A' . [x'/x]M_2' : \Pi z \dv A' . [x'/x]B'$$
and finally conclude
$$\Gamma, x\div A' \prov  \lambda z\dv A' . M_1' = \lambda z \dv A' . M_2' : \Pi z \dv A' . B'$$
or in other words
$$\Gamma \prov  M_1 = M_2 : A$$