def rev2

bend-osdev-crypto@0.1.0.0 · PROOF.bend:138

import Base
import bend-osdev-crypto@0.1.0.0/stream.bend as St

138def rev2(l: List<&2, U32>, +a: List<&2, U32>) -> {St.cr.rev_onto(St.cr.rev_onto(l, a), Nil{}) == St.cr.rev_onto(a, l) : List<&2, U32>}:
139  match l:
140    case Nil{}:
141      {==}
142    case Con{h, t}:
143      rev2(t, Con{h, a})