def cv_add

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

import bend-kit-collections@0.1.4.1/nat_order.bend as NatOrder

import Base

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

Uses (9)

Used by (36)