- renamed subtype to subtype_poly
- pi function does not have implicit arguments anymore
- changed a rewrite rule into an axiom
- added wip tuples