Nuprl - Pf st list mng wf

l:SimpleType List, rho:Decl{i}. [[l]] rho{i} Type{i'}

By: Analyze 0 THEN ListInd 1 THEN Unfold `st_list_mng` 0 THEN Reduce 0 THEN Try (Fold `st_list_mng` 0) THEN EasyHyp

Generated subgoals:

None

About: