"allow an Avail programmer to provide transformation rules[..], as long as she provides the corresponding proof to be checked." Impressive!