(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 <pohj...@chalmers.se> wrote: >> >> Try this: >> >> REWRITE_TAC [pairTheory.ELIM_UNCURRY] >> >> Cheers / Johannes >> >> >> On 2016-11-16 17:04, Scott Owens wrote: >>> 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 mailing list >>> hol-info@lists.sourceforge.net >>> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------ _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
