Export cofixpoints.
Export local contexts.
Rename constant types to be more standard and to mirror the arities of inductive types.
Export inductive definitions.