(45steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc

At: discrete Formula with rank 1 3 1 1
1. x: Formula
2. x2: Formula
3. x3: Formula
4. y:Formula. Dec(x2 = y)
5. y:Formula. Dec(x3 = y)
6. y@0: Formula
7. x5: Formula
8. x6: Formula

Dec(x2x3 = x5x6)
By:
DWith -2 -5
THEN
DWith -2 -5
Generated subgoal:

14. y@0: Formula
5. x5: Formula
6. x6: Formula
7. Dec(x2 = x5)
8. Dec(x3 = x6)
Dec(x2x3 = x5x6)

About:
decidableequalall

(45steps) PrintForm Definitions formula equality Sections ClassicalProps(jlc) Doc