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

At: discrete Formula with rank 1 5 1 1
1. x: Formula
2. y1: Formula
3. y2: Formula
4. y:Formula. Dec(y1 = y)
5. y:Formula. Dec(y2 = y)
6. y@0: Formula
7. y3: Formula
8. y4: Formula

Dec(y1y2 = y3y4)
By:
DWith -2 -5
THEN
DWith -2 -5
Generated subgoal:

14. y@0: Formula
5. y3: Formula
6. y4: Formula
7. Dec(y1 = y3)
8. Dec(y2 = y4)
Dec(y1y2 = y3y4)

About:
decidableequalall

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