def base_rev

bend-collections-laws-math@1.0.0.0 · proofs/lib/list.bend:230

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

230def base_rev(-A: Data, +xs: List<&2, A>) -> {List.reverse(&2, A, xs) == SC.reverse(A, xs) : List<&2, A>}:
231  Equal.trans(List<&2, A>, List.reverse.go(&2, A, xs, Nil{}), SC.append(A, SC.reverse(A, xs), Nil{}), SC.reverse(A, xs), base_rev_go(A, xs, Nil{}), append_nil(A, SC.reverse(A, xs)))