def append_nil

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/aes/ghash.bend:49

import Base

49def append_nil(+l: List<&2, Bool>) -> {List.append(&2, Bool, l, Nil{}) == l : List<&2, Bool>}:
50  match l:
51    case Nil{}:
52      {==}
53    case c <> r:
54      %append_nil(r) : {c <> List.append(&2, Bool, r, Nil{}) == c <> _ : List<&2, Bool>}
55      {==}