def oc.len

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:864

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-bytes@0.1.0.0/LAWS.bend as BL

864def oc.len(+o: B.Octets, +n: Nat, h: {B.Octets.len(o) == n : Nat}) -> {B.len(B.Octets.to_list(o)) == n : Nat}:
865  Equal.trans(Nat, B.len(B.Octets.to_list(o)), B.Octets.len(o), n, Equal.sym(Nat, B.Octets.len(o), B.len(B.Octets.to_list(o)), BL.octets_len_list(o)), h)

Uses (8)

Used by (2)