law cons_inj_t

lawful-arrays@0.1.0.0 · proof_base.bend:460

import Base

460law cons_inj_t:
461  for -A: Data
462  for -x: A
463  for -y: A
464  for -xs: List<&2, A>
465  for -ys: List<&2, A>
466  for e: {x <> xs == y <> ys : List<&2, A>}
467  {xs == ys : List<&2, A>}