(*************************** testing characters *******************************)
definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
definition is_bar ≝ λc:DeqUnialpha. c == bar.
(*************************** testing characters *******************************)
definition is_bit ≝ λc.match c with [ bit _ ⇒ true | _ ⇒ false ].
definition is_bar ≝ λc:DeqUnialpha. c == bar.