def append_nil

qasim-bend-kit@0.1.0.2 · proof/JSON_ListProof.bend:3

import Base

3def append_nil(-A: Data, +xs: List<&2, A>) -> {List.append(&2, A, xs, Nil{}) == xs : List<&2, A>}:
4    match xs:
5        case Nil{}: {==}
6        case h <> t:
7            Equal.cong(List<&2, A>, List<&2, A>, ys => h <> ys, List.append(&2, A, t, Nil{}), t, append_nil(A, t))