Thms list 3 autom Sections AutomataTheory 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