def perm_trans

bend-mathlib@0.8.1.0 · perm.bend:44

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

44# Permutation is transitive.
45def perm_trans(-A: Data, +xs: List<&2, A>, -ys: List<&2, A>, -zs: List<&2, A>, h1: K.perm(A, xs, ys), h2: K.perm(A, ys, zs)) -> K.perm(A, xs, zs):
46  (s1, e1) = h1
47  (s2, e2) = h2
48  +s1 = s1
49  +s2 = s2
50  (List.append(&2, Nat, s1, s2), internal_trans_eq(A, s1, s2, xs, ys, zs, e1, e2))