def false_true

bendtorch@1.3.0.0 · PROOF.bend:160

import Base

160# False == True is impossible: rewriting the goal Empty = disc(False) with it gives disc(True) = Unit
161def false_true(e: {False{} == True{} : Bool}) -> Empty:
162  %Equal.sym(Bool, False{}, True{}, e) : disc(_)
163  Unit{}