def internal_apply_invert

import bend-mathlib@0.8.1.0/perm.bend as Perm

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

286def internal_apply_invert(-A: Data, +s: List<&2, Nat>, +xs: List<&2, A>) -> {K.apply(A, internal_invert(s), K.apply(A, s, xs)) == xs : List<&2, A>}:
287  match s:
288    case Nil{}:
289      {==}
290    case +i <> rest:
291      %Equal.sym(List<&2, A>, K.apply(A, List.append(&2, Nat, internal_invert(rest), i <> Nil{}), K.apply(A, rest, K.swap_at(A, i, xs))), K.apply(A, i <> Nil{}, K.apply(A, internal_invert(rest), K.apply(A, rest, K.swap_at(A, i, xs)))), internal_apply_app(A, internal_invert(rest), i <> Nil{}, K.apply(A, rest, K.swap_at(A, i, xs)))) : {_ == xs : List<&2, A>}
292      %Equal.sym(List<&2, A>, K.apply(A, internal_invert(rest), K.apply(A, rest, K.swap_at(A, i, xs))), K.swap_at(A, i, xs), internal_apply_invert(A, rest, K.swap_at(A, i, xs))) : {K.apply(A, i <> Nil{}, _) == xs : List<&2, A>}
293      internal_swap_at_invol(A, i, xs)

Uses (9)

Used by (1)

bend-mathlib@0.8.1.0/perm:internal_sym_eq