Nuprl - Definition Cascade for ptn

	No other cites to report in MarkB_generic

ptn_int	`Def ptn_int(x) == inr(inl(x))`

	`Thm* T:Type, x:. ptn_int(x) ptn_con(T)`

	`Thm* x:. ptn_int(x) Pattern`

About: