test(tests/lean/run): direct subterm for non-reflexive datatype
test(tests/lean/run): add another subterm example
feat(library/definitional/projection): use strict implicit inference, closes #344