We will prove locally_connected ordered_square ordered_square_topology ∧ ¬ locally_path_connected ordered_square ordered_square_topology.

Apply andI to the current goal.

An exact proof term for the current goal is ordered_square_locally_connected.

An exact proof term for the current goal is ordered_square_not_locally_path_connected.

∎