def sc_take_zero
import bend-collections-laws-math@1.0.0.0/proofs/lib/list.bend as Listimport Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
323def sc_take_zero(-A: Data, +xs: List<&2, A>) -> {SC.take(A, xs, 0n) == Nil{} : List<&2, A>}:
324 match xs:
325 case Nil{}:
326 {==}
327 case Con{a, t}:
328 {==}