We will prove generated_topology EuclidPlane circular_regions = R2_standard_topology.

rewrite the current goal using circular_rectangular_same_topology_plane (from left to right).

An exact proof term for the current goal is generated_topology_rectangular_regions_eq_R2_standard_topology.

∎