Nuprl - Three Citations of Three case

Def case x: 3

case0; 3

case1; 3

case2; == InjCase(x; zero. case0; one_or_two. InjCase(one_or_two; one. case1; two. case2))

is not mentioned in this or prior sections.

Try larger context: ClassicalProps(jlc)