BackwardPROOF.append_ne: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 48-56 of bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&start_line=48&end_line=56

import Base

def append_ne(-A: Data, +xs: List<&2, A>, +item: A, +rest: List<&2, A>) ->
  {False{} == Nat.is_eq(List.length(&2, A, List.append(&2, A, xs, item <> rest)), List.length(&2, A, rest)) : Bool}:
  %Equal.sym(Nat, List.length(&2, A, List.append(&2, A, xs, item <> rest)),
    Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)), length_append(A, xs, item <> rest)) :
    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
  %Equal.sym(Nat, Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)),
    1n+Nat.add(List.length(&2, A, xs), List.length(&2, A, rest)), add_succ(List.length(&2, A, xs), List.length(&2, A, rest))) :
    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
  succ_add_ne(List.length(&2, A, xs), List.length(&2, A, rest))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=length_append
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=succ_add_ne