def cv_c

bend-kit-collections@0.1.4.1 · nat_order.bend:171

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

171def cv_c(+n: Nat, v: Vs) -> {n == F(L{n, 0n, 0n, 0n, 0n}, v) : Nat}:
172  match v:
173    case VS{v1, v2, v3, v4}:
174      sy(Nat.add(n, 0n), n, MNat.add_zero(n))