λA. A ∨ (¬A)

Definition decidable : Prop -> Prop := fun (A:Prop) => connectives.Or A (connectives.Not A)

definition decidable : Prop -> Prop := \lambda A : Prop. (Or) A ((Not) A)

def decidable : (Prop) -> Prop := fun (A : Prop) , (((connectives.Or) ) (A)) (((connectives.Not) ) (A))

decidable : [bool -> bool] = (LAMBDA(A:bool):connectives_sttfa_th.sttfa_Or(A)(connectives_sttfa_th.sttfa_Not(A)))

Printing for OpenTheory is not working at the moment.