[STATEMENT]
lemma rbd_Id_pres: "bd\<^sub>\<R> Id = id"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bd\<^sub>\<R> Id = id
[PROOF STEP]
unfolding rbd_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (bd\<^sub>\<F> \<circ> \<F>) Id = id
[PROOF STEP]
by simp