Nuprl - Pf decidable equal Three

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

At: decidable equal Three

x,y:. Dec(x = y)

By: UnivCD

Generated subgoal:

1 1. x:
2. y:
Dec(x = y)

About:

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