law foldr_cons_nil_sym

bend-mathlib@0.8.1.0 · list.bend:3055

import Base

3055# Folding cons from the right, starting from the empty list, rebuilds the list, reversed to rewrite toward the simple side.
3056law foldr_cons_nil_sym:
3057  for ~a: Quant
3058  for ~A: Kind(a)
3059  for xs: List<a, A>
3060  {xs == List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) : List<a, A>}