Nuprl - Pf st app1 wf

s1,s2:SimpleType. st_app1(s1;s2) Collection(SimpleType)

By: Unfold `st_app1` 0 THEN Unfold `st` 1 THEN TreeInd 1 THEN Reduce 0 THEN All (Fold `st`)

Generated subgoals:

None

About: