def true_false
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logicimport Base
16def true_false(e: {True{} == False{} : Bool}) -> Empty:
17 false_true(Equal.sym(Bool, True{}, False{}, e))
Uses (4)
Used by (18)
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:not_lt_le
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:not_le_lt
- bend-collections-laws-math@1.0.0.0/proofs/lib/nat:lt_or_eq
- bend-collections-laws-math@1.0.0.0/proofs/lib/arith:quot_lt_g
- bend-collections-laws-math@1.0.0.0/proofs/lib/arith:sc_lt_cancel_g
- …