Who Cites absval?
absval	Def |i| == if 0i i else -i fi
	Thm* x:. |x|
int_nzero	Def == {i:| i 0 }
	Thm* Type
nat_plus	Def == {i:| 0 < i }
	Thm* Type
le_int	Def ij == j < i
	Thm* i,j:. ij
nequal	Def a b T == a = b T
	Thm* A:Type, x,y:A. x y Prop
lt_int	Def i < j == if i < j true ; false fi
	Thm* i,j:. i < j
bnot	Def b == if b false else true fi
	Thm* b:. b
not	Def A == A False
	Thm* A:Prop. (A) Prop

About: