∀ {α : Type u_4} {β : α → Type u_5} {γ : (a : α) → β a → Type u_6} [inst : DecidableEq α]
  [inst_1 : (a : α) → DecidableEq (β a)] [inst_2 : (a : α) → (b : β a) → Zero (γ a b)] (i : (a : α) × β a)
  (x : γ i.fst i.snd), Sigma.curry (Pi.single i x) = Pi.single i.fst (Pi.single i.snd x)