Hi Chun,
use functional extensionality. There are many ways to do it, one is
using the theorem boolTheory.FUN_EQ_THM.
Best
Thomas
On 24.03.2017 21:42, Chun Tian (binghe) wrote:
> Hi again,
>
> If I have a theorem saying two (2-ary) relations are the same:
>
> |- R = R’
>
> Then I can easily prove the following theorem using REWRITE_TAC:
>
> |- !x y. R x y = R’ x y
>
> But if I had the second one first, how to prove the previous one?
>
> Regards,
>
> Chun Tian
>
>
>
>
> ------------------------------------------------------------------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
>
>
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
