-Added texified formal type system specification
-Some examples
-TODO