is mentioned by

Thm* l:SimpleType List, rho:Decl{i}. [[l]] rho{i} Type{i'}	[st_list_mng_wf]
Thm* t:eff(). t.typ SimpleType	[eff_typ_wf]
Thm* sts1,sts2:Collection(SimpleType), rho:Decl, v:[[sts1]] rho. sts1 = sts2 v [[sts2]] rho	[sts_mng_functionality]
Thm* t:SimpleType, rho:Decl, v:[[t]] rho. v [[ < t > ]] rho	[sts_mng_singleton]
Thm* sts:Collection(SimpleType), rho:Decl, v:[[sts]] rho, s:SimpleType. s sts v [[s]] rho	[sts_mng_subtype]
Thm* r:rel(), de:sig(), i:. tc1(r;de) i < ||r.args|| rel_arg_typ(r.name;i;de) SimpleType	[rel_arg_typ_wf]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 = a2 b1 = b2 st_app(a1;b1) = st_app(a2;b2)	[st_app_functionality]
Thm* a1,a2,b1,b2:Collection(SimpleType). a1 a2 b1 b2 st_app(a1;b1) st_app(a2;b2)	[st_app_monotone]
Thm* c1,c2:Collection(SimpleType), s:SimpleType. s st_app(c1;c2) (a:SimpleType. a c2 & as c1)	[member_st_app]
Thm* x:Label, a1,a2:Collection(dec()). a1 a2 dec_lookup(a1;x) dec_lookup(a2;x)	[dec_lookup_monotone]
Thm* ds1,ds2:Collection(dec()), x:Label. ds1 = ds2 dec_lookup(ds1;x) = dec_lookup(ds2;x)	[dec_lookup_functionality]
Thm* ds:Collection(dec()), x:Label, T:SimpleType. T dec_lookup(ds;x) mk_dec(x, T) ds	[member_dec_lookup]
Thm* t:frame(). t.typ SimpleType	[frame_typ_wf]
Thm* t:smt(). t.typ SimpleType	[smt_typ_wf]
Thm* t:dec(). t.typ SimpleType	[dec_typ_wf]
Thm* t:sig(). t.rel Label(SimpleType List)	[sig_rel_wf]
Thm* t:sig(). t.fun LabelSimpleType	[sig_fun_wf]
Thm* s1,s2,s:SimpleType. s st_app1(s1;s2) st_eq(s1;s2s)	[member_st_app1]
Thm* s1,s2:SimpleType. st_app1(s1;s2) Collection(SimpleType)	[st_app1_wf]
Def [[sts]] rho == x:{x:SimpleType| x sts }. [[x]] rho	[sts_mng]
Def eff() == LabelLabelSimpleTypesmt()	[eff]
Def st_app(c1;c2) == (s2c2.(s1c1.st_app1(s1;s2)))	[st_app]
Def single_valued_decls(c) == x:Label, t1,t2:SimpleType. mk_dec(x, t1) c mk_dec(x, t2) c t1 = t2	[single_valued_decls]
Def dec_lookup(ds;x) == < d.typ | d < d ds | d.lbl = x > >	[dec_lookup]
Def frame() == LabelSimpleType(Label List)	[frame]
Def relname() == SimpleType+Label	[relname]
Def smt() == LabelTermSimpleType	[smt]
Def dec() == LabelSimpleType	[dec]
Def sig() == (LabelSimpleType)(Label(SimpleType List))	[sig]
Def st_app1(s1;s2) == Case(s1) Case a;b = > if st_eq(a;s2) < b > else < > fi Default = > < >	[st_app1]

In prior sections: mb automata 1

Try larger context: GenAutomata