Thanks a lot! Also, the website states:
"As noted earlier, we can also easily convert any assertion T in closed form to its related assertion Ti in inference form by applying ax-mp <https://us.metamath.org/mpeuni/ax-mp.html>. The challenge, when working formally, can sometimes occur when converting some arbitrary assertion T in inference form into a related assertion Td in deduction form" Still, are there some examples or are there general guidelines that will help with this process? How would I go about converting Ti to Td in the example stated above (or from Ti to T)? Again, many thanks! Op dinsdag 15 augustus 2023 om 17:02:33 UTC+2 schreef [email protected]: > On 8/15/23 07:49, David A. Wheeler wrote: > > Maybe we should note something in trud. > > Ooh, good idea. I hadn't thought of that as a mitigation. Submitted as > https://github.com/metamath/set.mm/pull/3388 > > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/4fd884c5-e715-4465-8048-d73f4e82c30bn%40googlegroups.com.
