UNCURRY_CONV
PairRules.UNCURRY_CONV : conv
Uncurrys an application of an abstraction.
Example
> PairRules.UNCURRY_CONV (Term `(\x y. x + y) 1 2`);
val it = ⊢ (λx y. x + y) 1 2 = (λ(x,y). x + y) (1,2): thm
Failure
UNCURRY_CONV tm fails if tm is not double abstraction applied to two
arguments