Remove the existentials from top-level modules
In this MR we remove the existential types from the records of the top-level modules. This should help proving properties about modules and functors.
In this MR we remove the existential types from the records of the top-level modules. This should help proving properties about modules and functors.