law length_singleton_sym

bend-mathlib@0.8.1.0 · list.bend:3132

import Base

3132# A one-element list has length one, reversed to rewrite toward the simple side.
3133law length_singleton_sym:
3134  for -a: Quant
3135  for -A: Kind(a)
3136  for -x: A
3137  {1n == List.length(a, A, [x]) : Nat}