law append_inj_l

lawful-arrays@0.1.0.0 · proof_base.bend:472

import Base

472# Two appends with equally long first parts: the first parts are equal...
473law append_inj_l:
474  for -A: Data
475  for +x1: List<&2, A>
476  for +x2: List<&2, A>
477  for -y1: List<&2, A>
478  for -y2: List<&2, A>
479  for hl: {List.length(&2, A, x1) == List.length(&2, A, x2) : Nat}
480  for +e: {List.append(&2, A, x1, y1) == List.append(&2, A, x2, y2) : List<&2, A>}
481  {x1 == x2 : List<&2, A>}