Who Cites sm all?
sm_all	Def i:I M(i) == mk_sm(M(i).da for i I, M(i).ds for i I, s.i:I. M(i).init(s), s1,a,s2. i:I. M(i).trans(s1,a,s2))
sm_trans	Def t.trans == 2of(2of(2of(t)))
	Thm* M:sm{i:l}(). M.trans M.stateM.actionM.stateProp
sm_init	Def t.init == 1of(2of(2of(t)))
	Thm* M:sm{i:l}(). M.init M.stateProp
sm_ds	Def t.ds == 1of(2of(t))
	Thm* t:sm{i:l}(). t.ds Decl
dall	Def D(i) for i I(x) == i:I. D(i)(x)
	Thm* I:Type, D:(IDecl). D(i) for i I Decl
sm_da	Def t.da == 1of(t)
	Thm* t:sm{i:l}(). t.da Decl
mk_sm	Def mk_sm(da, ds, init, trans) == < da,ds,init,trans >
	Thm* da,ds:Decl, init:({ds}Prop), trans:({ds}(da){ds}Prop). mk_sm(da, ds, init, trans) sm{i:l}()
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

Syntax:

i:I M(i)

has structure:

sm_all(I; i.M(i))

About: