def internal_swap_head_invol

bend-mathlib@0.8.1.0 · perm.bend:256

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

256def internal_swap_head_invol(-A: Data, xs: List<&2, A>) -> {K.swap_head(A, K.swap_head(A, xs)) == xs : List<&2, A>}:
257  match xs:
258    case Nil{}:
259      {==}
260    case +x <> t:
261      match t:
262        case Nil{}:
263          {==}
264        case +y <> u:
265          {==}