def internal_swap_head_length

bend-mathlib@0.8.1.0 · perm.bend:305

import Base
import bendlib-kernel-list@1.0.0.0/list.bend as K

305def internal_swap_head_length(-A: Data, xs: List<&2, A>) -> {List.length(&2, A, K.swap_head(A, xs)) == List.length(&2, A, xs) : Nat}:
306  match xs:
307    case Nil{}:
308      {==}
309    case +x <> t:
310      match t:
311        case Nil{}:
312          {==}
313        case +y <> u:
314          {==}