Logic.true_not_false: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as Logic
Lines 55-56 of bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&start_line=55&end_line=56

import Base

def true_not_false(b: Bool, t: {b == True{} : Bool}, f: {b == False{} : Bool}) -> Empty:
  false_true(Equal.trans(Bool, False{}, b, True{}, Equal.sym(Bool, b, False{}, f), t))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=false_true