laziness tweak, typo

paper/gtt.tex

@@ -4508,7 +4508,7 @@ The following lemma shows this forms a computation ep pair:
 
 From this, we see that the easiest way to construct an interpretation
 of the dynamic computation type is to make it a lazy product of all
-the ground types $\u G$: $\dyns \cong \With_{\u G} \u G$.
+the ground types $\u G$: $\dync \cong \With_{\u G} \u G$.
 
 Using recursive types, we can easily make this a definition of the
 interpretations:
@@ -9383,8 +9383,9 @@ Finally note that once we have introduced the extra thunks to model
 difference between call-by-name and call-by-need is only relevant for
 performance reasons.
 %
-Therefore the resulting cast semantics we produce should also be
-valid for call-by-need evaluation.
+Since divergence and uncatchable errors are idempotent, and these are
+usually the only effects in lazy languages, the resulting cast
+semantics GTT produces should also be valid for call-by-need.
 
 \citet{Degen2012TheIO} give an analysis of different cast semantics
 for contracts in lazy languages, specifically based on Haskell, so