On Tuesday, May 28, 2019 at 9:25:47 PM UTC+2, Giovanni Mascellani wrote: > > Hi! I think there is a general trick to replace a $d x A or $d x ph$ > condition in a theorem with the corresponding F/_ x A or F/ x ph, but I > do not remember it. Can anybody help me? >
> (in this specific case, I would like to do that for sbcex2 and its > universal counterpart) > Hi Giovanni. I think that by now, most utility theorems with dv conditions have an analogous "nf-version" where the dv conditions are replaced with non-freeness $e-hypotheses. In your example sbcex2, it looks like it is sufficient to replace: exlimiv with exlimi, exbidv with exbid, vtoclbg with vtoclbgf. Generally, the labels are found by adding a suffixed "f" or removing a suffixed "v". I'm not sure there is a completely automatizable method to find the nf-proof from a dv-proof, but there are certainly recurring patterns. > PS. I already asked the same question on the Metamath Gitter channel[1], > but I believe it is not very active at the moment! > > [1] https://gitter.im/metamath/Lobby I did not know of this channel. Maybe it would be nice to centralize discussions on this group and forget/close the other ones? Benoît -- 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/c6698e19-c68f-494d-b2e3-0dd6f980ff2b%40googlegroups.com.
