Nuprl - Pf decidable equal Three 1 7

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

At: decidable equal Three 1 7

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