Change `DatatypeVerificationTests.lean` to use concrete syntax

[joscoh]

Once the DDM fully supports datatypes (including polymorphic and mutually recursive ones), we no longer need tests with explicit AST nodes, so the tests in DatatypeVerificationTests.lean should be removed or changed to ones with concrete syntax.