@@ -252,7 +252,7 @@ property of subject reduction.\beppe{Example?}

Finally, there is one last rule in our type system, the one that

implements occurrence typing, that is, the rule for the

type-case:\beppe{Changed to \Rule{If} to \Rule{Case}}

type-case:

\begin{mathpar}

\Infer[Case]

...

...

@@ -312,7 +312,7 @@ To ease our analysis we used different directions for each kind of

term. So we have $0$ and $1$ for the function and argument of an

application, $l$ and $r$ for the $l$eft and $r$ight expressions forming a pair,

and $f$ and $s$ for the argument of a $f$irst or of a $s$econd projection. Note also that we do not consider occurrences

under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).\beppe{Is it what I wrote here true?}

under $\lambda$'s (since their type is frozen in their annotations) and type-cases (since they reset the analysis).

The judgments $\Gamma\evdash e t \Gamma'$ are then deduced by the following two rules: \begin{mathpar}