Let X, Tx and n be given.

Assume Hdim: covering_dimension X Tx n.

Apply Hdim to the current goal.

Assume Hcore Hrest.

Apply Hcore to the current goal.

Assume HTx Hn.

An exact proof term for the current goal is Hn.

∎