def internal_list_nat_append_assoc

bend-mathlib@0.8.1.0 · algebra.bend:118

import Base
import bend-mathlib@0.8.1.0/list.bend as MList

118def internal_list_nat_append_assoc(x: List<&2, Nat>, y: List<&2, Nat>, z: List<&2, Nat>) -> {List.append(&2, Nat, List.append(&2, Nat, x, y), z) == List.append(&2, Nat, x, List.append(&2, Nat, y, z)) : List<&2, Nat>}:
119  MList.append_assoc(&2, Nat, x, y, z)