[STATEMENT]
lemma register_tensor_id_update[simp]:
  assumes \<open>register F\<close>
  shows \<open>register (\<lambda>a::'a::type update. F a \<otimes>\<^sub>u Some)\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (\<lambda>a. F a \<otimes>\<^sub>u Some)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
register F

goal (1 subgoal):
 1. register (\<lambda>a. F a \<otimes>\<^sub>u Some)
[PROOF STEP]
apply (rule register_comp[unfolded o_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. register (\<lambda>a. a \<otimes>\<^sub>u Some)
[PROOF STEP]
by simp