start towards OpenTheory compatibility for relation and pred_set

This is potentially going to be complicated since OpenTheory defines a
type of sets and HOL4 does not.

import function package from OpenTheory standard library