Hi Thomas, Sorry, I found and tried FUN_EQ_THM, but failed to see the path to benefit from it ...
> Il giorno 24 mar 2017, alle ore 21:50, Thomas Tuerk <[email protected]> > ha scritto: > > 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
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ 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
