def aria_d22
import bend-osdev-legacy-ciphers@0.1.0.0/PROOF.bend as PROOFimport Base
import bend-osdev-legacy-ciphers@0.1.0.0/aria.bend as A
8349def aria_d22(+s: A.LcAriaSt) -> {s == A.aria.u22(A.aria.d22(s)) : A.LcAriaSt}:
8350 %aria_e21(A.aria.d21(s)) : {s == A.aria.u21(_) : A.LcAriaSt}
8351 aria_d21(s)