An exact proof term for the current goal is (basis_refines_topology X T C Htop HCsub Href).