Filling Cubes and h-Level

[kangrongji]

This PR finishes the proof that a type is of h-level n if and only if any n-boundary can be extended to an n-cube. It is possible to make a macro to automatically transform this internal formulation to an external one using partial element, which seems more direct and easier to use. Examples are given at the end of Cubical.Foundations.Cubes. Would it be the first Cubical Solver?