Thms bool 1 Doc

bool Def == Unit+Unit

Thm* Type

guard Def {T} == T

Thm* {T} Type

btrue Def true ==

Thm* true

bfalse Def false ==

Thm* false

function_primDef x:AB(x) == PRIMITIVE {Total functions from A: x.b(x) such that b(x) B(x) for x A }