law cons_inj_h

lawful-arrays@0.1.0.0 · proof_base.bend:448

import Base

448law cons_inj_h:
449  for -A: Data
450  for -x: A
451  for -y: A
452  for -xs: List<&2, A>
453  for -ys: List<&2, A>
454  for e: {x <> xs == y <> ys : List<&2, A>}
455  {x == y : A}