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

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

Dec(x2x3 = x5x6)
By:
FalseCase
THEN
Analyze -3
Generated subgoal:

17. Dec(x3 = x6)
8. x2x3 = x5x6
x2 = x5

About:
decidableequal

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