def fit_len

bend-osdev-aead@0.1.0.0 · PROOF.bend:211

import Base
import bend-osdev-bytes@0.1.0.0/bytes.bend as B
import bend-osdev-aead@0.1.0.0/authenc.bend as Au

211def fit_len(n: Nat, xs: List<&2, U32>) -> {B.len(Au.ad.au.fit(n, xs)) == n : Nat}:
212  match n:
213    case 0n:
214      {==}
215    case 1n+m:
216      match xs:
217        case Nil{}:
218          %fit_len(m, Nil{}) : {1n+B.len(Au.ad.au.fit(m, Nil{})) == 1n+_ : Nat}
219          {==}
220        case Con{h, t}:
221          %fit_len(m, t) : {1n+B.len(Au.ad.au.fit(m, t)) == 1n+_ : Nat}
222          {==}