[STATEMENT]
lemma uniformity_transfer[transfer_rule]:
  "(rel_filter (rel_prod A A)) uniformity uniformity"
  if [transfer_rule]: "bi_total A"  "bi_unique A" "(A ===> A ===> (=)) dist dist"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_filter (rel_prod A A) uniformity uniformity
[PROOF STEP]
unfolding uniformity_dist
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. rel_filter (rel_prod A A) (INF e\<in>{0<..}. principal {(x, y). dist x y < e}) (INF e\<in>{0<..}. principal {(x, y). dist x y < e})
[PROOF STEP]
by transfer_prover