TensorBackwardPROOF.other_operand: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend as TensorBackwardPROOF
Lines 147-156 of bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward_PROOF.bend&start_line=147&end_line=156

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def other_operand(x: Bool, y: Bool, both: {Bool.and(x, Bool.not(y)) == True{} : Bool}) -> {y == False{} : Bool}:
  match x:
    case False{}:
      Empty.absurd({y == False{} : Bool}, Arith.clash(both))
    case True{}:
      match y:
        case True{}:
          Empty.absurd({True{} == False{} : Bool}, Arith.clash(both))
        case False{}:
          {==}

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=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash