def rr_back

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

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

515# a structural list, reversed onto Nil and back, is itself
516def rr_back(+zs: List<&2, U32>) -> {B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, U32>}:
517  Equal.trans(List<&2, U32>, B.rev_onto(B.rev_onto(zs, Nil{}), Nil{}), List.append(&2, U32, zs, Nil{}), zs, ru_rr(zs, Nil{}, Nil{}), app_nilu(zs))