def con_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixbytes.bend:31

import Base

31def con_eq(+x: Nat, +y: Nat, xs: List<&2, Nat>, ys: List<&2, Nat>, +ex: {x == y : Nat}, +ets: {xs == ys : List<&2, Nat>}) -> {Con{x, xs} == Con{y, ys} : List<&2, Nat>}:
32  Equal.trans(List<&2, Nat>, Con{x, xs}, Con{y, xs}, Con{y, ys}, Equal.cong(Nat, List<&2, Nat>, t => Con{t, xs}, x, y, ex), Equal.cong(List<&2, Nat>, List<&2, Nat>, t => Con{y, t}, xs, ys, ets))