def li.last_app

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1448

import Base
import bend-osdev-cipher-modes@0.1.0.0/cipher_modes.bend as M
import bend-osdev-cipher-modes@0.1.0.0/xts.bend as T

1448def li.last_app(es: List<&2, M.CmBlock>, +x: M.CmBlock, +e: M.CmBlock) -> {T.xts.last(List.append(&2, M.CmBlock, es, Con{x, Nil{}}), e) == x : M.CmBlock}:
1449  match es:
1450    case Nil{}:
1451      {==}
1452    case Con{+e2, +es2}:
1453      li.last_app(es2, x, e2)