My long standing question:
How to eliminate writing $\cap^L$ instead of plain $\cap$ when we deal with more than one lattice? (and likewise with other (finite and infinite) structures) It is especially boring when $L$ is more than one math symbol but a more complex expression.
Can we do something like disjoint union of all lattices? It seems this problem is somehow solved in Mizar, but I don't know Mizar (despite of the fact that I'm familiar with Isabelle/ISAR). BTW, can you provide me with a readable introduction into Mizar's type system?