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

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

Dec(y1y2 = y3y4)
By:
FalseCase
THEN
Analyze -2
Generated subgoal:

18. y1y2 = y3y4
y2 = y4

About:
decidableequal

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