NOTE:

This operator coercing a to a Prop is normally invisible since it is pretty obvious when it is needed.

	Who Cites assert?
assert	Def b == if b True else False fi
	Thm* b:. b Prop
iff	Def P Q == (P Q) & (P Q)
	Thm* A,B:Prop. (A B) Prop
list_all	Def xL.P(x) == (letrec list_all L = (Case of L; nil True ; h.t P(h) & list_all(t)) ) (L)
	Thm* T:Type, P:(TProp), L:T List. xL.P(x) Type
	Thm* T:Type, P:(TType). xnil.P(x) Type
list_all_2	Def xL.P(x) == (letrec all L = (Case of L; nil true ; h.t P(h)(all(t))) ) (L)
	Thm* T:Type, P:(T), L:T List. xL.P(x)
rev_implies	Def P Q == Q P
	Thm* A,B:Prop. (A B) Prop
letrec_body	Def = b == b
letrec_arg	Def x b(x) (x) == b(x)
letrec	Def (letrec f b(f)) == b((letrec f b(f)) ) (recursive)
band	Def pq == if p q else false fi
	Thm* p,q:. (pq)

About: