Nuprl - Pf K and equal Three 2 1

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

At: K and equal Three 2 1

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

x = 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