No TPTP formula. May not be expressible in strict first order. | Merge.kif 3369-3369 | Funcao Injetiva e' uma sub-classe de funcao Unaria |
No TPTP formula. May not be expressible in strict first order. | Merge.kif 3387-3387 | Funcao Sequencia e' uma sub-classe de Funcao Injetiva |