Merge pull request #1170 from jeanas/grammar

Minor grammar fix

Author: mikeshulman

preliminaries.tex

@@ -474,7 +474,7 @@ \section{Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)}
 \indexdef{application!of dependent function}%
 \indexdef{function!dependent!application}%
 As with non-dependent functions, we can \define{apply} a dependent function $f : \prd{x:A}B(x)$ to an argument $a:A$ to obtain an element $f(a):B(a)$.
-The equalities are the same as for the ordinary function type, i.e.\ we have the computation rule
+The equalities are the same as for the ordinary function type, i.e.\ we have the following computation rule:
 \index{computation rule!for dependent function types}%
 given $a:A$ we have $f(a) \jdeq \Phi'$ and  
 $(\lamu{x:A} \Phi)(a) \jdeq \Phi'$, where $\Phi' $ is obtained by replacing all