diff --git a/papers/icfp2021/figure-pipeline-inv.tex b/papers/icfp2021/figure-pipeline-inv.tex
index e425ff41f44a704e6c23bdb8aab7f4dd1f6e9d5a..f44c5d7d0fcd9eacfecb22276e2e35d2726fc9ea 100644
--- a/papers/icfp2021/figure-pipeline-inv.tex
+++ b/papers/icfp2021/figure-pipeline-inv.tex
@@ -35,12 +35,12 @@
 %\multicolumn{3}{r}{%
 
       \left\{\begin{array}{l}
-          \Exists \curf, \curg, \yElemViewListInv<\curg><\curf>*[].
+          \Exists \curf, \curg, \tview, \hview, \yElemViewListInv<\curg><\curf>*[].
       \\  \quad \ISep{%
                   \curg \leq \curf
             \isep \ownGhost \gcurf {\authfull \curf}
             \isep \ownGhost \gcurg {\authfull \curg}
-            \cr   \isQueue \emptyview \emptyview {\yElemViewListInv<\curg><\curf>}
+            \cr   \isQueue \tview \hview {\yElemViewListInv<\curg><\curf>}
             \cr   \displaystyle\Sep_{\curg \leq \idx < \curf}
                     \left(\wpre {g\;\yElem_\idx} {\Lam z. R\;\idx\;z}\right) \opat \view_\idx
           }%end of the main \ISep of the invariant