TyInf: simplify presentation of schemes
TyInf: simplify presentation of schemes

We need to define :: as a map to an implication, rather than by a rule, so that
we can apply it. It seems to be neater to define >=> the other way, so it uses
a context suffix (rather than having to introduce the notion of scheme prefix).
We may as well also define
  (Xi >=> tau) \scheme   =   Xi >- tau type
so lemma 10 becomes immediate.


mietek/epigram2,mietek/epigram2,larrytheliquid/pigit