Components of the proof are there, but it hasnt been put together. In the master branch Model.UnstructuredUniverse contains a definition of unstructured Id. In the clans branch Model.StructuredModel contains a definition of structured Id. Part of the equivalence (the elimination bit) was proven for natural models - its in the master branch Model.Natural.NaturalModel and is called toId and toId'. Sorry for the mess, but I can help tidy this up with whoever wants to take on this task.
Components of the proof are there, but it hasnt been put together. In the master branch
Model.UnstructuredUniversecontains a definition of unstructuredId. In the clans branchModel.StructuredModelcontains a definition of structuredId. Part of the equivalence (the elimination bit) was proven for natural models - its in the master branchModel.Natural.NaturalModeland is calledtoIdandtoId'. Sorry for the mess, but I can help tidy this up with whoever wants to take on this task.