def cons_cong

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/list.bend:8

import Base

8def cons_cong(-A: Data, +h: A, +xs: List<&2, A>, +ys: List<&2, A>, +e: {xs == ys : List<&2, A>}) -> {Con{h, xs} == Con{h, ys} : List<&2, A>}:
9  Equal.cong(List<&2, A>, List<&2, A>, zs => Con{h, zs}, xs, ys, e)