Express and enforce well-formedness of (mutual) ADTs

[joscoh]

Mutual blocks of ADTs have a variety of checks (e.g. strict positivity, uniformity, non-emptiness, non-nesting, topological ordering of type references) that are checked in TypeFactory.addMutualBlock. We should define a predicate MutualBlockWF (either as part of TypeFactory or externally) and show that the typechecker enforces this predicate. This predicate is currently an implicit precondition to some functions (e.g. genBlockFactory) but should be made explicit.