law list_nat_append_assoc4_sym

bend-mathlib@0.8.1.0 · algebra.bend:466

import Base

466# Four-way reassociation for List append over Nat, reversed to rewrite toward the simple side.
467law list_nat_append_assoc4_sym:
468  for +a: List<&2, Nat>
469  for +b: List<&2, Nat>
470  for +c: List<&2, Nat>
471  for +d: List<&2, Nat>
472  {List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) == List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) : List<&2, Nat>}