law is_empty_reverse

bend-mathlib@0.8.1.0 · list.bend:1871

import Base

1871# The reverse is empty exactly when the list is.
1872law is_empty_reverse:
1873  for -a: Quant
1874  for -A: Kind(a)
1875  for xs: List<a, A>
1876  {List.is_empty(a, A, List.reverse(a, A, xs)) == List.is_empty(a, A, xs) : Bool}