(Re)implement partial elements

[ice1000]

Re #446. Needed for hcom.

Plan:

• Add PartialTyTerm in the xtt package, with Term lhs, Term rhs, Term ty as data. It can be type-checked as a prim, making it easier to write. The type is Partial : (r s : I) -> Type -> Set.
• Implement the conversion of PartialTyTerm: if the logical formula rhs = lhs is mutually implied by lhs' = rhs' and A unifies with A', then Partial lhs rhs A unifies with Partial lhs' rhs' A'.
• Add PartialTerm in the xtt package, with its syntax, parsing, producing, etc.. This is going to be a bit more laborious.
• Implement the conversion of PartialTerm.

[ice1000]

The prim definition is done in 3c9226c