Nuprl - Pf lshort_wf 1

PrintForm Definitions list 3 autom Sections AutomataTheory Doc

At: lshort wf 1

1. St: Type
2. l: St*
3. eq: StSt

LShort(l) St*

By: ListInd 2 THEN RecUnfold `lshort` 0 THEN Reduce 0

Generated subgoals:

None

About: