def AP.set_length

bend-osdev-array@0.1.0.1 · PROOF.bend:1475

import Base

1475def AP.set_length(-T: Data, xs: List<&2, T>, k: Nat, -v: T) -> {List.length(&2, T, List.set(&2, T, xs, k, v)) == List.length(&2, T, xs) : Nat}:
1476  match xs k:
1477    case Nil{} _:
1478      {==}
1479    case Con{x, t} 0n:
1480      {==}
1481    case Con{x, t} 1n+p:
1482      AP.succ_cong(List.length(&2, T, List.set(&2, T, t, p, v)), List.length(&2, T, t), AP.set_length(T, t, p, v))