DISP	parec_df	parec(<A:A-var>,<x:x-var>.<B:B:*> @ <a:a:*>) == parec(<A>,<x>.<B> @ <a>)
ABS	parec	parec(A,x.B[A; x] @ a) == !null_abstraction{}
DISP	parec_ind_df	parec_ind(<r:r:*><h:var>,<z:var>.<t:t:*>) == parec_ind(<r><h>,<z>.<t>)
ABS	parec_ind	parec_ind(r;h,z.t[h; z]) == !null_abstraction{}
DISP	mono_df	Mono{<i:level>}(<b:b-var>,<x:x-var>.<B:B:*> on <T:T:*>) == Mono{<i>}(<b>,<x>.<B> on <T>)
ABS	mono	Mono{i}(b,x.B[b; x] on T) == b',b'':T . (x:T. b' x b'' x) (x:T. B[b'; x] B[b''; x])
THM	mono_wf	T:. B:(T ) T . Mono{i}(b,x.B[b;x] on T) '
RULE	parecEquality	H, parec(b1,x1.B1 @ t1) = parec(b2,x2.B2 @ t2) BY parecEquality T x b b1' b2' u v H t1 = t2 H, x:T, b:T B1[b,x/b1,x1] = B2[b,x/b2,x2] H Mono{i}(b1,x1.B1 on T)
RULE	parecMemberFormation	H, parec(b,x.B @ a) ext t BY parecMemberFormation level{i} z H B[(z.parec(b,x.B @ z)),a/b,x] ext t H parec(b,x.B @ a)
RULE	parecMemberEquality	H, b1 = b2 BY parecMemberEquality level{i} z H b1 = b2 H parec(b,x.B @ t)
RULE	parecElimination	H, t:T, J, r:parec(b,x.B @ t), J1, G ext parec_ind(t;t',h.g[(x.)/u]) BY parecElimination level{i} #$j1 #$j2 b' u h t' v H, t:T, J, r:parec(b,x.B @ t), J1, b':T u:t':T. b' t' parec(b,x.B @ t'), h:t':T. b' t' G[t'/t] t':T, v:B[b',t'/b,x] G[t'/t] ext g
RULE	parecUnrollElimination	H, r:parec(b,x.B @ t), J, G ext g[r/r'] BY parecUnrollElimination #$i r' z u H, r:parec(b,x.B @ t), J, r':B[(z.parec(b,x.B @ z)),t/b,x], u:r = r' G[r'/r] ext g
RULE	parec_indEquality	H, parec_ind(r1;h1,z1.t1) = parec_ind(r2;h2,z2.t2) BY parec_indEquality level{i} (x.S[x/r1]) (a:A parec(A,x.B @ a)) Z u h z H r1 = r2 H, Z:A , u:z:(a:A Z a) (z = z), h:z:(a:A Z a) S[z/x] z:a:A B[Z/A][a/x] t1[h/h1][z/z1] = t2[h/h2][z/z2]
DISP	positive_df	positive(<n:n:*>)== positive(<n>)
ABS	positive	positive(n) == parec(p,x.x = 1 p (x - 1) @ n)
THM	positive_wf	z:. positive(z)
THM	gt0_imp_pos	z:. z > 0 positive(z)
THM	pos_imp_gt0	z:. positive(z) z > 0

the other theories