Nuprl - Pf K not wf 1 1

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

At: K not wf 1 1

1. p:

case p: 3 3; 3 3; 3 3;

By: ThreeInd 1 THEN AbReduce 0

Generated subgoals:

None

About:

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