Theorem prod.ext

fix(*): untangle dependency hierarchy

feat(tactic/ext): `ext` now applies to `prod`; fix `ext` on function types (#158)

feat(analysis/metric_space): sup metric for product of metric spaces