def perm_refl

bend-mathlib@0.8.1.0 · perm.bend:27

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

27# Permutation is reflexive.
28def perm_refl(-A: Data, -xs: List<&2, A>) -> K.perm(A, xs, xs):
29  (Nil{}, {==})