def append_ne

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:48

import Base

48def append_ne(-A: Data, +xs: List<&2, A>, +item: A, +rest: List<&2, A>) ->
49  {False{} == Nat.is_eq(List.length(&2, A, List.append(&2, A, xs, item <> rest)), List.length(&2, A, rest)) : Bool}:
50  %Equal.sym(Nat, List.length(&2, A, List.append(&2, A, xs, item <> rest)),
51    Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)), length_append(A, xs, item <> rest)) :
52    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
53  %Equal.sym(Nat, Nat.add(List.length(&2, A, xs), 1n+List.length(&2, A, rest)),
54    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))) :
55    {False{} == Nat.is_eq(_, List.length(&2, A, rest)) : Bool}
56  succ_add_ne(List.length(&2, A, xs), List.length(&2, A, rest))