Def (l) == null(l)

Thm* Alph:Type. LangOver(Alph)

Def null(as) == Case of as; nil true ; a.as' false

Thm* T:Type, as:T*. null(as)

Thm* null(nil)

Def b == if b True else False fi

Thm* b:. b Prop