law empty_eq

lawful-bytes@0.1.1.0 · proof_grow.bend:48

import Base
import lawful-bytes@0.1.1.0/defs.bend as D
import lawful-bytes@0.1.1.0/bytes.bend as B
import lawful-bytes@0.1.1.0/proof_core.bend as C

48law empty_eq:
49  for +d: Nat
50  {B.empty(d) == C.BT(0, tnew(d, 0)) : D.Bytes}