def internal_swap_at_invol

bend-mathlib@0.8.1.0 · perm.bend:267

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

267def internal_swap_at_invol(-A: Data, +i: Nat, +xs: List<&2, A>) -> {K.swap_at(A, i, K.swap_at(A, i, xs)) == xs : List<&2, A>}:
268  match i:
269    case 0n:
270      internal_swap_head_invol(A, xs)
271    case 1n+p:
272      match xs:
273        case Nil{}:
274          {==}
275        case +x <> t:
276          %Equal.sym(List<&2, A>, K.swap_at(A, p, K.swap_at(A, p, t)), t, internal_swap_at_invol(A, p, t)) : {x <> _ == x <> t : List<&2, A>}
277          {==}