(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:
decidableequal

(17steps) PrintForm Definitions Three Sections ClassicalProps(jlc) Doc