law last_append_singleton

bend-mathlib@0.8.1.0 · list.bend:1777

import Base

1777# The last element of xs ++ [x] is x.
1778law last_append_singleton:
1779  for -a: Quant
1780  for -A: Kind(a)
1781  for xs: List<a, A>
1782  for -x: A
1783  {List.last(a, A, List.append(a, A, xs, [x])) == Some{x} : Maybe<a, A>}