NatOrder.cv_add: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder
Lines 192-195 of bend-kit-collections@0.1.4.1/nat_order.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&start_line=192&end_line=195

import Base

def cv_add(-A: Nat, -B: Nat, +p: Lin, +q: Lin, +v: Vs, eA: {A == F(p, v) : Nat}, eB: {B == F(q, v) : Nat})
  -> {Nat.add(A, B) == F(ladd(p, q), v) : Nat}:
  tr(Nat.add(A, B), Nat.add(F(p, v), F(q, v)), F(ladd(p, q), v),
    cong_add(A, F(p, v), B, F(q, v), eA, eB), F_add(p, q, v))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=F
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=F_add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Lin
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=Vs
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=cong_add
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=ladd
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/nat_order.bend&name=tr