law foldr_cons_nil

bend-mathlib@0.8.1.0 · list.bend:1925

import Base

1925# Folding cons from the right, starting from the empty list, rebuilds the list.
1926law foldr_cons_nil:
1927  for ~a: Quant
1928  for ~A: Kind(a)
1929  for xs: List<a, A>
1930  {List.foldr(~a, ~A, ~List<a, A>, ~(x => acc => x <> acc), xs, Nil{}) == xs : List<a, A>}