def gt.rep_len

bend-osdev-gf@0.1.1.0 · proof_tab.bend:242

import Base

242def gt.rep_len(+n: Nat) -> {List.length(&2, U32, List.replicate(U32, n, 0)) == n : Nat}:
243  match n:
244    case 0n:
245      {==}
246    case 1n+k:
247      %Equal.sym(Nat, List.length(&2, U32, List.replicate(U32, k, 0)), k, gt.rep_len(k)) : {1n+_ == 1n+k : Nat}
248      {==}