law length_singleton

bend-mathlib@0.8.1.0 · list.bend:2081

import Base

2081# A one-element list has length one.
2082law length_singleton:
2083  for -a: Quant
2084  for -A: Kind(a)
2085  for -x: A
2086  {List.length(a, A, [x]) == 1n : Nat}