def pair_bounded

bendtorch-core@0.1.0.0 · src/autograd/tensor_backward_PROOF.bend:291

import Base
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward_LAWS.bend as Laws

291def pair_bounded(+a: Nat, +b: Nat, +bound: Nat) ->
292  {Bool.and(Nat.is_lt(a, bound), Nat.is_lt(b, bound)) == Laws.bounded([a, b], bound) : Bool}:
293  Equal.cong(Bool, Bool, flag => Bool.and(Nat.is_lt(a, bound), flag), Nat.is_lt(b, bound), Bool.and(Nat.is_lt(b, bound), True{}),
294    Equal.sym(Bool, Bool.and(Nat.is_lt(b, bound), True{}), Nat.is_lt(b, bound), and_true(Nat.is_lt(b, bound))))