[STATEMENT]
lemma unitaryD2[simp]: "unitary U \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. unitary U \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun
[PROOF STEP]
unfolding unitary_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. U* o\<^sub>C\<^sub>L U = id_cblinfun \<and> U o\<^sub>C\<^sub>L U* = id_cblinfun \<Longrightarrow> U o\<^sub>C\<^sub>L U* = id_cblinfun
[PROOF STEP]
by simp