Level: Lib Thy Top:
Hypotheses:

None

Conclusion:

T:. U:{j}. V:{k}. f:(T U) V. f = uncurry curry f

Applied Tactic: Unfolds ``curry uncurry`` 0 THEN Auto
Generated subgoals:

1. f = (x.let <l,r> = x in (x,y.f <x, y>) l r)