Nuprl - Pf decidable equal Three 1 4

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

At: decidable equal Three 1 4

Dec(3 = 3)

By: Choose [2] THEN Analyze 0

Generated subgoal:

1 1. 3 = 3
False

About:

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