law slice_zero

lawful-bytes@0.1.1.0 · proof_append.bend:84

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

84law slice_zero:
85  for +xs: List<&2, U32>
86  for +i: Nat
87  {D.slice(xs, i, 0n) == Nil{} : List<&2, U32>}