Implement OTT universe
Better use of notation
Implement coercion
Add refl, Resp, subst
Remove mutual block
Get rid of non-standard vacuous equality
Merge pull request #11 from darinmorrison/ott

Implement OTT universe