def natural_equal_true

bendtorch-core@0.1.0.0 · src/tensor/allocation_PROOF.bend:51

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

51def natural_equal_true(+a: Nat, +b: Nat, equal: {a == b : Nat}) -> {True{} == Nat.is_eq(a, b) : Bool}:
52  Equal.sym(Bool, Nat.is_eq(a, b), True{},
53    Equal.trans(Bool, Nat.is_eq(a, b), Nat.is_eq(b, b), True{},
54      Equal.cong(Nat, Bool, n => Nat.is_eq(n, b), a, b, equal), Arith.eq_refl(b)))