law is_empty_reverse_sym

bend-mathlib@0.8.1.0 · list.bend:3024

import Base

3024# The reverse is empty exactly when the list is, reversed to rewrite toward the simple side.
3025law is_empty_reverse_sym:
3026  for -a: Quant
3027  for -A: Kind(a)
3028  for xs: List<a, A>
3029  {List.is_empty(a, A, xs) == List.is_empty(a, A, List.reverse(a, A, xs)) : Bool}