ふつう、A =_def B から A = B を導く推論なんて考えずに、A =_def B
と A = B を式として同一視するんじゃない？ それはつまり=_defを等号
と同一視しているってことじゃない？