λb. if b then false else true

Definition notb : bool -> bool := fun (b:bool) => match_bool_type (bool) false true b

definition notb : bool -> bool := \lambda b : bool. (match_bool_type) (bool) (false) (true) b

noncomputable def notb : (bool.bool) -> bool.bool := fun (b : bool.bool) , ((((bool.match_bool_type) (bool.bool)) ((bool.false) )) ((bool.true) )) (b)

notb : [bool_sttfa.sttfa_bool -> bool_sttfa.sttfa_bool] = (LAMBDA(b:bool_sttfa.sttfa_bool):bool_sttfa.match_bool_type[bool_sttfa.sttfa_bool](bool_sttfa.sttfa_false)(bool_sttfa.sttfa_true)(b))

Printing for OpenTheory is not working at the moment.