def append_length

qasim-bend-kit@0.1.0.2 · proof/AES_ZipLengthProof.bend:116

import Base

116def append_length(+xs: List<&2, U32>, +ys: List<&2, U32>) ->
117    {List.length(&2, U32, List.append(&2, U32, xs, ys)) ==
118     Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}:
119    match xs:
120        case Nil{}: {==}
121        case x <> tail:
122            Equal.cong(Nat, Nat, n => 1n+n,
123                List.length(&2, U32, List.append(&2, U32, tail, ys)),
124                Nat.add(List.length(&2, U32, tail),
125                    List.length(&2, U32, ys)),
126                append_length(tail, ys))