def internal_append_nil

bend-mathlib@0.8.1.0 · perm.bend:110

import Base

110def internal_append_nil(-A: Data, +ys: List<&2, A>) -> {List.append(&2, A, ys, Nil{}) == ys : List<&2, A>}:
111  match ys:
112    case Nil{}:
113      {==}
114    case +y <> t:
115      %Equal.sym(List<&2, A>, List.append(&2, A, t, Nil{}), t, internal_append_nil(A, t)) : {y <> _ == y <> t : List<&2, A>}
116      {==}