law join_push

lawful-fields@0.1.1.0 · proof_list.bend:120

import Base
import lawful-fields@0.1.1.0/defs.bend as F

120law join_push:
121  for +x: U32
122  for +r: List<&2, List<&2, U32>>
123  for +sep: U32
124  {F.join(F.split.push(x, r), sep) == x <> F.join(r, sep) : List<&2, U32>}