DISP	min_ar_df	MinAr(<f:bool-fun:*><i:i:*><n:n:*>)== MinAr(<f><i><n>)
ML	min_ar_ml	MinAr(f;i;n)==r if f (n - i) =b f n then i else MinAr(f;i - 1;n) fi
THM	min_ar_wf	f: . n:. i:(n + 1). MinAr(f;i;n) (i + 1)
THM	min_ar_alt	f: . n:. i:(n + 1). j:((n - i) + 1). f (n - i) = f n MinAr(f;j + i;n) = MinAr(f;j;n - i) + i
THM	min_ar_sound	f: . n:. i:(n + 1). f (n - MinAr(f;i;n)) = f n
DISP	min_arg_df	MinArg(<f:f:*> : {0..<n:n:*>})== MinArg(<f> : {0..<n>})
ABS	min_arg	MinArg(f : {0..n}) == n - MinAr(f;n;n)
THM	min_arg_wf	f: . n:. MinArg(f : {0..n}) (n + 1)
THM	comb_for_min_arg_wf	(f,n,z.MinArg(f : {0..n})) f:( ) n: True (n + 1)
THM	min_arg_unique	f: . n,k:. f n = f k MinArg(f : {0..n}) = MinArg(f : {0..k})
THM	min_arg_sound	f: . n:. f MinArg(f : {0..n}) = f n
THM	min_arg_iff	f: . n,k:. f n = f k MinArg(f : {0..n}) = MinArg(f : {0..k})
DISP	min_el_df	Min{ x | x<E:E:*><n:n:*> }== Min{ x | x<E><n> }
ABS	min_el	Min{ x | xEn } == MinArg(E n : {0..n})
THM	min_el_wf	E: . n:. Min{ x | xEn }
THM	equiv_rel_fun	T:. E:T T . s,t:T. EquivRel(T;x,y.(x E y)) (s E t) E s = E t
THM	min_el_unique	E: . n,k:. EquivRel(;x,y.(x E y)) (n E k) Min{ x | xEn } = Min{ x | xEk }
THM	min_el_sound	E: . n:. EquivRel(;x,y.(x E y)) (n E Min{ x | xEn })
THM	min_el_iff	E: . n,k:. EquivRel(;x,y.(x E y)) ((n E k) Min{ x | xEn } = Min{ x | xEk })
THM	decide_imp_bool	T:. R:T T . (x,y:T. Dec(x R y)) (r:T T . x,y:T. (x r y) x R y)
THM	comp_choice	E: EquivRel(;x,y.x E y) (x,y:. Dec(x E y)) (h: . (n,k:. n E k h n = h k) (n:. n E (h n)))

the other theories