On Fri, Oct 29, 2021 at 2:30 PM Benoit <[email protected]> wrote:

> Mario: why, when you encounter a dummy class variable in the original
> proof, don't you simply use a dummy setvar variable in place of it ?
>

That works too. Any expression that doesn't use class variables will work
there.

-- 
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/CAFXXJSvOQ1oM5o3eL_PQ7_3Kq5_RcYx3Tze94VbGdBj-TxYnSA%40mail.gmail.com.

Reply via email to