Create stuck bindings for fun and profit (type errors, postulates)

[Blaisorblade]

• Support (and test) postulates (fix Support postulates. #95).
• Have declared identifiers available in client code even if their implementation does not typecheck (fix If a definition fails, all users trigger errors #98) — so errors in them don't cause errors at every usage.
• Improve testing infrastructure to automatically test everything under examples/.

[Blaisorblade]

This seems to work.
To test, I took Data/Pair1.lpts, and introduced a bug in cons1, which has a type annotation. Now users of cons1 don't get any more "Unbound identifier" errors.

./Data/Pair1.lpts:8.60-8.62: Type error: we expected two terms to be equivalent but they are not.
  The function has an unexpected codomain.
  Checked term: k a
  Actual type: B -> R
  But we expected type: R
  Difference
    actual:   B -> R
    expected: R     

  cons1 (A B : *) : A -> B -> Pair1 A B = lambda a b R k . k a;
                                                           ^^^

./Data/Pair1.lpts:13.20-13.24: Unbound identifier: cons1

  lambda f g p . cons1 B D (f (fst1 A C p)) (g (snd1 A C p));
                 ^^^^^

Automating this test depends on #94, but I could add files to examples/neg.

Then, I turned cons1 into a postulate, and the code compiled with no error. However, because of limitations of the parser support, I needed to desugar by hand the telescope:

postulate cons1 : Pi (A B : *). A -> B -> Pair1 A B;

However, the limitation is trivial to fix, since postulates reuse the code for bindings (and just omit the body).

[Blaisorblade]

Just rebased on top of master (also to fix merge conflicts).