I changed the document such that the equality type is now a CAS field which is not automatically generated.
The main benefit is a capacity for really nice equality types.
The drawback is needing to define equality types for every CAS record. Also, every equality proof for Casanova will have to be rewritten in terms of whatever the new equality type ends up being. Happily, the proofs were kind of messy, anyway.
I changed the document such that the equality type is now a CAS field which is not automatically generated.
The main benefit is a capacity for really nice equality types. The drawback is needing to define equality types for every CAS record. Also, every equality proof for Casanova will have to be rewritten in terms of whatever the new equality type ends up being. Happily, the proofs were kind of messy, anyway.