Negative typecheck tests

[arthurpaulino]

We want our typechecker to throw errors when checking any pair of term and type that shouldn't typecheck.

A way of achieving some level of confidence in this direction is by getting a decently long list of term/type pairs such that no two pairs of types are defeq and then trying to check some permutations and expecting them to fail. Example:

Suppose we have the following pairs of terms and types:

(te1, ty1), (te2, ty2), (te3, ty3)

Then the following shouldn't typecheck for any pair:

(te1, ty2), (te2, ty3), (te3, ty1)