Nuprl - Pf decidable equal Three 1 4 1

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

At: decidable equal Three 1 4 1

1. 3 = 3

False

By: ThreeNEQ 1

Generated subgoals:

None

About:

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