(Re²)implement partial elements

[ice1000]

Re #1293: we actually do need to deal with more-than-one clauses in partials, for convenience of implementing the argument of hcom. We will need to support this:

partial {
| i = j => M₁
| k = i => M₂
| k = j => M₃
}

And the type checking of this term will make sure things like i = j, k = i ⊢ M₁ = M₂.

Then, we will write partial types using a syntax of cofibration expressions. So we will need disjunctions. I don't right now see any use of conjunctions, so we do not have to do it.