Add mutually recursive types to Lambda

[joscoh]

Description of changes:
Adds mutually recursive types to Lambda and its corresponding SMT generation (declare-datatypes). In particular, mutually recursive types generate multiple eliminators, which still have the expected computational behavior. This PR includes tests in TypeFactoryTests.lean for eliminators, other derived functions, and typechecking and in SMTEncoderDatatypeTest.lean and DatatypeVerificationTest.lean for SMT output and verification.
Some key changes:

1. Core declarations can now have multiple declarations (and likewise multiple names)
2. The SMT output becomes simpler. We no longer need dependency analysis to rule out mutually recursive types, instead checking type references when a mutual block is created and therefore maintaining a topological order.
3. Substantial changes to the proofs in ProgramWF.lean, which now have more structure but also more repetition. They can/should be improved in a future PR.

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[shigoel]

We no longer need dependency analysis to rule out mutually recursive types, instead checking type references when a mutual block is created and therefore maintaining a topological order.

So, so nice!

[shigoel]

Partial review for now.

[MikaelMayer]

This PR adds mutually recursive types to Lambda, which is a significant and well-implemented feature. The implementation is thorough with comprehensive tests covering eliminators, testers, destructors, and error cases. The SMT encoding has been simplified by maintaining topological order in the TypeFactory. Overall, this is solid work that extends the type system in a principled way.

Critical issue: There is a bug in validateMutualBlock that prevents duplicate name detection. This should be fixed before merging.

[shigoel]

Left some questions/comments. Looks great, thanks!