No TPTP formula. May not be expressible in strict first order. | Merge.kif 3369-3369 | One to one function is a subclass of unary function |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3387-3387 | Sequence function is a subclass of one to one function |