s1,s2,s:SimpleType. s 
st_app1(s1;s2) 
st_eq(s1;s2
s)
s2c2.(s1c1.st_app1(s1;s2)))
< b > else < > fi Default = > < >
is mentioned by
| Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s) | [member_st_app1] |
| Def st_app(c1;c2) == (s2c2.(s1c1.st_app1(s1;s2))) | [st_app] |
Try larger context:
GenAutomata