def shift_shift

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

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index

574def shift_shift(+a: Nat, +b: Nat, +xs: List<&2, Nat>) -> {shift(a, shift(b, xs)) == shift(Nat.add(a, b), xs) : List<&2, Nat>}:
575  match xs:
576    case Nil{}:
577      {==}
578    case +x <> +rest:
579      %Equal.sym(Nat, Nat.add(a, Nat.add(b, x)), Nat.add(Nat.add(a, b), x), Index.add_assoc(a, b, x)) : {_ <> shift(a, shift(b, rest)) == Nat.add(Nat.add(a, b), x) <> shift(Nat.add(a, b), rest) : List<&2, Nat>}
580      Equal.cong(List<&2, Nat>, List<&2, Nat>, tail => Nat.add(Nat.add(a, b), x) <> tail,
581        shift(a, shift(b, rest)), shift(Nat.add(a, b), rest), shift_shift(a, b, rest))