Skip to content
Snippets Groups Projects
Commit ec564a10 authored by Max New's avatar Max New
Browse files

one more lemma we'll need

parent 91c85d90
No related branches found
No related tags found
No related merge requests found
......@@ -1044,7 +1044,7 @@ is our graduality theorem.
\begin{mathpar}
\inferrule
{A \ltdyn A'}
{}
{\cdots}
\end{mathpar}
\end{lemma}
......@@ -1092,6 +1092,11 @@ Finally, we reach the case-by-case proof of the graduality lemma.
\end{enumerate}
\end{lemma}
\begin{lemma}[Graduality Substitution Principles]
TODO: substituting value in a value, term or stack, substituting a
term in a stack (use substitution for the target, decomposition)
\end{lemma}
\begin{figure}
\begin{mathpar}
\begin{array}{rcl}
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment