Enable btree_predicate_proof() to make proofs involving cross-data-type

predicate operators.  The hard stuff turns out to be already done in the
previous commit, we need merely open the floodgates...