def revrev

bend-osdev-acpi@0.1.1.0 · PROOF_tables.bend:247

import Base

247def revrev(-A: Data, +xs: List<&2, A>) -> {xs == List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})) : List<&2, A>}:
248  Equal.trans(List<&2, A>, xs, List.append(&2, A, xs, Nil{}), List.reverse(&2, A, List.reverse.go(&2, A, xs, Nil{})), gapp_nil(A, xs), rev_app(A, xs, Nil{}, Nil{}))