An exact proof term for the current goal is (andEL (metric_on X d) (total_function_on d (setprod X X) R) H).