actualize array-perm with nat by morphism :array → arrnat; :elem → nat; mkarray → mkarray; ] → ]; ] → ]; # → #; #oc → #oc; perm → perm; a → n2; b → n3; c → n4; ar → A; ar0 → A0; ar1 → A1; ar2 → A2 end actualize