∀ b, (b = true) ∨ (b = false)

Theorem true_or_false : forall (b:bool), connectives.Or (logic.eq (bool) b true) (logic.eq (bool) b false).

theorem true_or_false : \forall (b:bool). (Or) ((eq) (bool) b (true) ) ((eq) (bool) b (false) ).

theorem true_or_false : forall (b:bool.bool) , (((connectives.Or) ) ((((logic.eq_) (bool.bool)) (b)) ((bool.true) ))) ((((logic.eq_) (bool.bool)) (b)) ((bool.false) )).

true_or_false : LEMMA (FORALL(b:bool_sttfa.sttfa_bool):connectives_sttfa_th.sttfa_Or(logic_sttfa_th.eq[bool_sttfa.sttfa_bool](b)(bool_sttfa.sttfa_true))(logic_sttfa_th.eq[bool_sttfa.sttfa_bool](b)(bool_sttfa.sttfa_false)))

Printing for OpenTheory is not working at the moment.