Nuprl - Definition Cascade for outr

	No other cites to report in MarkB_generic

outr	`Def outr(x) == InjCase(x; y. "???"; z. z)`

	`Thm* A,B:Type, x:A+B. isl(x) outr(x) B`

About: