Level:
Lib
Thy
Top
:
Hypotheses:
None
Conclusion:
T:
.
U:
{j}.
V:
{k}.
f:T
U
V. f = curry uncurry f
Applied Tactic:
RA(D 0)
Generated subgoals:
1
. f = curry uncurry f
T:
. U:{j}. V:{k}. f:T 
U V. f = curry uncurry f