def reverse_twice

qasim-bend-kit@0.1.0.2 · proof/JSON_ListProof.bend:76

import Base

76def reverse_twice(-A: Data,
77                  +xs: List<&2, A>) -> {List.reverse(&2, A, List.reverse(&2, A, xs)) == xs : List<&2, A>}:
78    Equal.trans(List<&2, A>, List.reverse(&2, A, List.reverse(&2, A, xs)), List.append(&2, A, xs, Nil{}), xs,
79        reverse_shift(A, xs, Nil{}, Nil{}), append_nil(A, xs))