Remove now-irrelevant todo

0xd34df00d · Nov 4, 2020 · dbf9416 · dbf9416
1 parent f8778ca
commit dbf9416
Showing 1 changed file with 0 additions and 2 deletions.
diff --git a/tex/paper.mng b/tex/paper.mng
@@ -372,8 +372,6 @@ this is a well-founded proof.
   as it invokes the substitution lemma (\cref{lma:type_substitution}).
 \end{proof}
 
-\todo[inline]{What to do about the assumptions on the well-formedness of target context in oracle assumptions vs the Agda formal proof that doesn't do that?}
-
 \subsection{Core language}
 
 The syntax of the core language is presented in \figref{core_syntax},