Definitions MarkB generic Sections NuprlLIB Doc

No other cites to report in MarkB_generic
case_enum1_el2Def enum1_el2 = > body cont(x,z) == InjCase(if x=1 inl(*) ; inr(*) fi ; body; cont(z,z))

Syntax:enum1_el2 = > body cont has structure: case_enum1_el2(body; cont)

About:
natural_numberint_eqinlinr
decideapplyaxiom
!abstraction

Definitions MarkB generic Sections NuprlLIB Doc