Introduce witness pairs: pairs of variables where the first one is the
witness for the second one.  Introduce variants of Pi, lambda, ev, that
handle that and make the witness checker handle them.