[STATEMENT]
lemma norm_transfer[transfer_rule]:
  "(A ===> (=)) norm norm"
  if [transfer_rule]: "(A ===> A ===> (=)) inner inner"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=)) norm norm
[PROOF STEP]
unfolding norm_eq_sqrt_inner
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (A ===> (=)) (\<lambda>x. sqrt (x \<bullet> x)) (\<lambda>x. sqrt (x \<bullet> x))
[PROOF STEP]
by transfer_prover