Def ActionSet(T) == car:TypeTcarcar

Thm* T:Type{i}. ActionSet(T) Type{i'}

Thm* T:Type, a:ActionSet(T). a.car Type

Def b == if b True else False fi

Thm* b:. b Prop

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

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

Thm* null(nil)

Thm* A:Type, B:(AType), p:a:AB(a). 1of(p) A