Finished proof of admissibility of transitivity.
Improved comments in Type.Context; minor changes in Header file.