I didn't know about ELIM_UNCURRY - cool!
I would have done rw[GSYM pairTheory.LAMBDA_PROD] (after trying a bunch of
things that didn't work..)
Also, rw[FORALL_DEF,Once FUN_EQ_THM,pairTheory.UNCURRY] seems to work.
As for where this goal came from, I've seen it coming from EVAL_TAC before.
On 17
(forgot to reply to list the first time)
On 2016-11-16 17:35, Scott Owens wrote:
> Thanks, that works.
>
> For the curious, the ELIM_UNCURRY theorem is ``∀f. UNCURRY f = (λx. f (FST x)
> (SND x))``. Not obviously relevant...
>
> Scott
>
>> On 2016/11/16, at 16:23, Johannes Åman Pohjola
Does anyone know how to prove this goal:
∀(p1,p1',p2). T
I’m not sure how I got it, and I can’t work out how to prove it, but it’s
probably true :)
Scott
--
___
hol-info
