def shift_append

bendtorch-core@0.1.0.0 · src/autograd/reduce_fiber_proof.bend:565

import Base

565def shift_append(+base: Nat, +xs: List<&2, Nat>, +ys: List<&2, Nat>) ->
566  {shift(base, List.append(&2, Nat, xs, ys)) == List.append(&2, Nat, shift(base, xs), shift(base, ys)) : List<&2, Nat>}:
567  match xs:
568    case Nil{}:
569      {==}
570    case +x <> +rest:
571      Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => Nat.add(base, x) <> tail,
572        shift(base, List.append(&2, Nat, rest, ys)), List.append(&2, Nat, shift(base, rest), shift(base, ys)), shift_append(base, rest, ys))