law get_cons_zero

bend-mathlib@0.8.1.0 · list.bend:1692

import Base

1692# The element at index zero of a cons is its head.
1693law get_cons_zero:
1694  for -a: Quant
1695  for -A: Kind(a)
1696  for -x: A
1697  for -xs: List<a, A>
1698  {List.get(a, A, x <> xs, 0n) == Some{x} : Maybe<a, A>}