law is_empty_append_sym

bend-mathlib@0.8.1.0 · list.bend:3013

import Base

3013# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
3014law is_empty_append_sym:
3015  for -a: Quant
3016  for -A: Kind(a)
3017  for xs: List<a, A>
3018  for -ys: List<a, A>
3019  {Bool.and(List.is_empty(a, A, xs), List.is_empty(a, A, ys)) == List.is_empty(a, A, List.append(a, A, xs, ys)) : Bool}