:| Equal < \N:Natural, \M:Natural >
	ReflEQ < x:Natural > -> Equal<x,x>

:| GreaterEqual < \N:Natural, \M:Natural >
    ReflGE < x:Natural > -> GreaterEqual<x, x>
	SuccGE < x:Natural, y:Natural, ge:GreaterEqual<x,y> > -> GreaterEqual< Succ(x), y >

:| Sig <\A:*, \P:A->*>
	exist < a:A, p:P(a) >

:| Sig2 <\A:*, \P:A->*, \Q:A->*>
	exist2 < a:A, p:P(a), q:Q(a) >

array_index ( array:Array<A>, index:Sig<Natural, GreaterEqual<length_of(array)> ) -> A