bool.not_eq_true_false
¬(true = false)
Theorem not_eq_true_false : connectives.Not (logic.eq (bool) true false).
theorem not_eq_true_false : (Not) ((eq) (bool) (true) (false) ).
theorem not_eq_true_false : ((connectives.Not) ) ((((logic.eq_) (bool.bool)) ((bool.true) )) ((bool.false) )).
not_eq_true_false : LEMMA connectives_sttfa_th.sttfa_Not(logic_sttfa_th.eq[bool_sttfa.sttfa_bool](bool_sttfa.sttfa_true)(bool_sttfa.sttfa_false))
Printing for OpenTheory is not working at the moment.