Let X, B and T be given.

Assume HBasis HT HBsub.

An exact proof term for the current goal is (generated_topology_finer X B T HBasis HT HBsub).

∎