law append_assoc

bend-ml-nat-lemmas@0.1.2.0 · main.bend:242

import Base

242law append_assoc:
243  for -A: Data
244  for  xs: List<&2, A>
245  for  ys: List<&2, A>
246  for  zs: List<&2, A>
247  {List.append(&2, A, List.append(&2, A, xs, ys), zs) == List.append(&2, A, xs, List.append(&2, A, ys, zs)) : List<&2, A>}