Thms
bool
1
Doc
NOTE:
The operator coercing a
to a Prop is normally invisible since it is pretty obvious when it is needed.
assert
Def
b == if b
True else False fi
Thm*
b:
. b
Prop
ifthenelse
Def
if b
t else f fi == dec(b ; t; f)
Thm*
b:
, A:Type, p,q:A. if b
p else q fi
A