diff --git a/docs/language/informal/local-inference.md b/docs/language/informal/local-inference.md
index 0b653c8..6810644 100644
--- a/docs/language/informal/local-inference.md
+++ b/docs/language/informal/local-inference.md
@@ -29,11 +29,9 @@
 Note that the closure of a type schema is a proper type.
 
 Note that the least closure of a type schema is always a subtype of any type
-which matches the schema, and the greatest closure of is always a supertype of
+which matches the schema, and the greatest closure is always a supertype of
 any type which matches the schema.
 
-
-
 ### Type variable elimination (least and greatest closure of a type)
 
 We define the least closure of a type `M` with respect to a set of type
@@ -42,9 +40,9 @@
 with `Object`.
 
 We define the greatest closure of a type `M` with respect to a set of type
-variables `T0, ..., Tn` to be `M` with every contravariant occurrence of `Ti`
-replaced with `Null`, and every covariant occurrence of `Ti` replaced with
-`Object`.
+variables `T0, ..., Tn` to be `M` with every covariant occurrence of `Ti`
+replaced with `Object`, and every contravariant occurrence of `Ti` replaced with
+`Null`.
 
 TODO(leafp): Specify this precisely
 
@@ -94,7 +92,7 @@
 The motivation for these operations is that constraint generation may produce a
 constraint on a type variable from an outer scope (say `S`) that refers to a
 type variable from an inner scope (say `T`).  For example, ` <T>(S) -> int <:
-<T>(List<T> -> int ` constrains `List<T>` to be a subtype of `S`.  But this
+<T>(List<T>) -> int ` constrains `List<T>` to be a subtype of `S`.  But this
 constraint is ill-formed outside of the scope of `T`, and hence if inference
 requires this constraint to be generated and moved out of the scope of `T`, we
 must approximate the constraint to the nearest constraint which does not mention
@@ -114,16 +112,16 @@
 
 The merge of constraint set `C` for a type variable `T` is a pair of types `Mb
 <: T <: Mt` defined as follows:
-  - let `Mt` be the lower bound of the `Mi` such that `T <: Mi` is in `C`
+  - Let `Mt` be the lower bound of the `Mi` such that `T <: Mi` is in `C`
       (and `?` if there are no subtype bounds for T in `C`)
-  - let `Mb` be the upper bound of the `Mi` such that `Mi <: T` is in `C` (and
+  - Let `Mb` be the upper bound of the `Mi` such that `Mi <: T` is in `C` (and
       `?` if there are no supertype bounds for T in `C`)
 
 #### Constraint solution for a type variable
 
 The constraint solution for a type variable `T` with respect to a constraint set
 `C` is defined as follows:
-  - let `Mb <: T <: Mb` be the merge of `C` with respect to `T`.
+  - Let `Mb <: T <: Mb` be the merge of `C` with respect to `T`.
   - If `Mb` is known (that is, it does not contain `?`) then the solution is
     `Mb`
   - Otherwise, if `Mt` is known (that is, it does not contain `?`) then the
@@ -135,7 +133,7 @@
 
 The grounded constraint solution for a type variable `T` with respect to a
 constraint set `C` is define as follows:
-  - let `Mb <: T <: Mb` be the merge of `C` with respect to `T`.
+  - Let `Mb <: T <: Mb` be the merge of `C` with respect to `T`.
   - If `Mb` is known (that is, it does not contain `?`) then the solution is
     `Mb`
   - Otherwise, if `Mt` is known (that is, it does not contain `?`) then the
@@ -237,7 +235,7 @@
   - If `R<B0, ..., Bj>` is the superclass of `P<M0, ..., Mk>` and `R<B0, ...,
 Bj>` is a subtype match for `Q<N0, ..., Nj>` with respect to `L` under
 constraints `C`.
-  - Or `R<B0, ..., Bj>` is one of the interfaces implemented by `P<M0, ..., Mk>` 
+  - Or `R<B0, ..., Bj>` is one of the interfaces implemented by `P<M0, ..., Mk>`
 (considered in lexical order) and `R<B0, ..., Bj>` is a subtype match for `Q<N0,
 ..., Nj>` with respect to `L` under constraints `C`.
   - Or `R<B0, ..., Bj>` is a mixin into `P<M0, ..., Mk>` (considered in lexical
@@ -344,7 +342,7 @@
   - If `C` does not constrain `Ti` then `Pi` is `?`
   - If `C` partially constrains `Ti`
     - If `C` is over constrained, then it is an inference failure error
-    - Otherwise `Pi` is the constraint solution for `Ti` with respect to `C` 
+    - Otherwise `Pi` is the constraint solution for `Ti` with respect to `C`
   - If `C` fully constrains `Ti`, then
     - Let `Ai` be `Bi[R0/T0, ..., ?/Ti, ..., ?/Tn]`
     - If `C + Ti <: Ai` is over constrained, it is an inference failure error.
@@ -362,7 +360,7 @@
 generic method of type `<T0 extends B0, ..., Tn extends Bn>(P0, ..., Pk) -> Q`
 given actual argument types `R0, ..., Rk`, a partial solution `[T0 -> P0, ...,
 Tn -> Pn]` and a partial constraint set `Cp`:
-  - If `Ri <: Pi [T0, ..., Tn] -> Ci` 
+  - If `Ri <: Pi [T0, ..., Tn] -> Ci`
   - And the full constraint resolution of `Cp + C0 + ... + Cn` for `<T0 extends
 B0, ..., Tn extends Bn>` given the initial partial solution `[T0 -> P0, ..., Tn
 -> Pn]` is `[T0 -> M0, ..., Tn -> Mn]`
@@ -452,7 +450,7 @@
   - And `<T0 extends B0, ..., Tn extends Bn>(P0, ..., Pk) -> Q` resolves via
 upwards resolution to a full solution `[T0 -> M0, ..., Tn -> Mn]`
     - Given partial solution `[T0 -> Q0, ..., Tn -> Qn]`
-    - And partial constraint set `Cp` 
+    - And partial constraint set `Cp`
     - And actual argument types `R0, ..., Rk`
   - And `N` is `Q[M0/T0, ..., Mn/Tn]`
 - A constructor invocation is inferred exactly as if it were a static generic
@@ -496,5 +494,5 @@
 inference, and compute the upper bound of all returned values for upwards
 inference.  Appropriate adjustments for asynchronous and generator functions.
 
-Do statements 
+Do statements
 For each statement