Bindings get bubbled as early in the sequence of bindings/conditions as possible

Define Element type

'true' conditions get filtered out

added pretty printing for termination checker

This reverts commit 8e6cfbae.

alternations

anyway)

Fixed ExprOps.isValue for covariant/contravariant function types.

MatchExpr considered as IfExpr.

2. Evaluation of invariants caches result for valid forall-invariant
interactions