∀ {D : Type u_1} {Q : Type u_2} (left : Q → D) (right : Q) (left_1 : Q → D) (right_1 : Q),
  ({ left := left, right := right } = { left := left_1, right := right_1 }) = (left = left_1 ∧ right = right_1)