law head_cons

bend-mathlib@0.8.1.0 · list.bend:1636

import Base

1636# The head of a cons is its first element.
1637law head_cons:
1638  for -a: Quant
1639  for -A: Kind(a)
1640  for -x: A
1641  for -xs: List<a, A>
1642  {List.head(a, A, x <> xs) == Some{x} : Maybe<a, A>}