Nuprl - Pf K and equal Three 2 2

(3steps) PrintForm Definitions Kleene Sections ClassicalProps(jlc) Doc

At: K and equal Three 2 2

1. x:
2. y:
3. x y = 3

y = 3

By: ThreeInd 2 THEN ThreeInd 1 THEN Reduce -1 THEN Try (ThreeNEQ 1)

Generated subgoals:

None

About:

(3steps) PrintForm Definitions Kleene Sections ClassicalProps(jlc) Doc