diff options
Diffstat (limited to 'docs/opt-coercion/fc-normalization-rta.tex')
| -rwxr-xr-x | docs/opt-coercion/fc-normalization-rta.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/docs/opt-coercion/fc-normalization-rta.tex b/docs/opt-coercion/fc-normalization-rta.tex index a1e7d4201d..c3bf41bd81 100755 --- a/docs/opt-coercion/fc-normalization-rta.tex +++ b/docs/opt-coercion/fc-normalization-rta.tex @@ -802,7 +802,7 @@ $$ \gamma ; \sym{\gamma} & \rsa{} & \refl{\tau} & \text{if}\,\gamma : \tau \psim \phi \end{array} $$ -But ther are much more complicated rewrites to consider. +But there are much more complicated rewrites to consider. Consider these coercions, where $C_N$ is the axiom generated by the newtype coercion in Section~\ref{sec:newtype}: $$ |