Question from Filip about milpgame proof assistant

[Norman Megill]

Filip asked me to post this.
Norm

-------- Forwarded Message --------
Subject: New feature of proof assistant
Date: Thu, 19 Nov 2020 13:35:16 +0000 (UTC)
From: Cernatescu Filip 
To: Norman Megill

Hi Norman!

I want to put a question on metamath forum:

I was thinking about a new feature on milpgame proof assistant:
If we have a complex metamath statement , we select only: (  (  ( A - 1 ) x. ( 2 x.  C )  ) /  (  (  A - 1)  x.  ( 3  x.  B ) )  ) and we put milpgame to search on set.mm. Milpgame it will give us some choices: divcan1i, divcan2i ,bla bla , we select one and milpgame will generate for us new statements, first: ( ( A - 1 ) x. ( 2 x. C ) ) /  ( ( A - 1 ) x. ( 3 x. B )  ) ) = ( ( 2 x. C  ) /  ( 3  x.  B ) ) and the following statements to be proven :  ( A - 1) e. CC  ,  (  2 x. C ) e. CC , ( 2 x. B ) e. CC. What do you say about that? It will be useful?

Thank you very much!