law some_inj

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aead/sound.bend:29

import Base

29law some_inj:
30  for +x: List<&2, U32>
31  for +p: List<&2, U32>
32  for +h: {Some{x} == Some{p} : Maybe<&2, List<&2, U32>>}
33  {x == p : List<&2, U32>}