def len_rev

bend-collections-laws-math@1.0.0.0 · proofs/lib/two_list.bend:61

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

61def len_rev(-T: Data, +xs: List<&2, T>) -> {SC.length(T, SC.reverse(T, xs)) == SC.length(T, xs) : Nat}:
62  LL.length_rev(T, xs)