Who Cites ioa all?
ioa_all	Def ioa_all(I; i.A(i)) == mk_ioa(i:I. A(i).ds, i:I. A(i).da, i:I. A(i).init, i:I. A(i).pre, i:I. A(i).eff, i:I. A(i).frame)
ioa_frame	Def t.frame == 2of(2of(2of(2of(2of(t)))))
col_union	Def (i:I. C(i))(x) == i:I. x C(i)
	Thm* T,I:Type, C:(ICollection(T)). (i:I. C(i)) Collection(T)
ioa_eff	Def t.eff == 1of(2of(2of(2of(2of(t)))))
ioa_pre	Def t.pre == 1of(2of(2of(2of(t))))
ioa_init	Def t.init == 1of(2of(2of(t)))
ioa_da	Def t.da == 1of(2of(t))
ioa_ds	Def t.ds == 1of(t)
mk_ioa	Def mk_ioa(ds, da, init, pre, eff, frame) == < ds,da,init,pre,eff,frame >
pi2	Def 2of(t) == t.2
	Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p))
col_member	Def x c == c(x)
	Thm* T:Type, x:T, c:Collection(T). x c Prop
pi1	Def 1of(t) == t.1
	Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A

About: