Formalise joins of simplices (Section 3.3 from RS17 paper)

[fizruk]

Should be straightforward, except definitions in Rzk would likely have to be duplicated for different concrete dimensions.

[jonalfcam]

I'm working on this a bit as an exercise.