law head_cons_sym

bend-mathlib@0.8.1.0 · list.bend:2869

import Base

2869# The head of a cons is its first element, reversed to rewrite toward the simple side.
2870law head_cons_sym:
2871  for -a: Quant
2872  for -A: Kind(a)
2873  for -x: A
2874  for -xs: List<a, A>
2875  {Some{x} == List.head(a, A, x <> xs) : Maybe<a, A>}