(17steps)
PrintForm
Definitions
Three
Sections
ClassicalProps(jlc)
Doc
At:
decidable
equal
Three
1
1.
x:
2.
y:
Dec(x = y)
By:
ThreeInd 1
THEN
ThreeInd 1
Generated subgoals:
1
Dec(3
= 3
)
2
Dec(3
= 3
)
3
Dec(3
= 3
)
4
Dec(3
= 3
)
5
Dec(3
= 3
)
6
Dec(3
= 3
)
7
Dec(3
= 3
)
8
Dec(3
= 3
)
9
Dec(3
= 3
)
About:
(17steps)
PrintForm
Definitions
Three
Sections
ClassicalProps(jlc)
Doc