def ru_rr

bend-osdev-bytes@0.1.1.0 · PROOF.bend:234

import Base
import bend-osdev-bytes@0.1.1.0/bytes.bend as B

234def ru_rr(xs: List<&2, U32>, acc: List<&2, U32>, b: List<&2, U32>) -> {B.rev_onto(B.rev_onto(xs, acc), b) == B.rev_onto(acc, List.append(&2, U32, xs, b)) : List<&2, U32>}:
235  match xs:
236    case Nil{}:
237      {==}
238    case Con{h, t}:
239      ru_rr(t, Con{h, acc}, b)