~/jendhub

def rr8_back

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

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

736def rr8_back(+zs: List<&2, B.OctByte>) -> {B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}) == zs : List<&2, B.OctByte>}:
737  Equal.trans(List<&2, B.OctByte>, B.w8s.rev_onto(B.w8s.rev_onto(zs, Nil{}), Nil{}), List.append(&2, B.OctByte, zs, Nil{}), zs, r8_rr(zs, Nil{}, Nil{}), app_nil8(zs))

Uses (7)

Used by (1)