def same_trans

bendtorch-core@0.1.0.0 · src/autograd/gradient_PROOF.bend:101

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

101def same_trans(-a: Core.Dynamic, -b: Core.Dynamic, -c: Core.Dynamic,
102  -ab: Totality.SameSource(a, b), -bc: Totality.SameSource(b, c)) -> Holds<Totality.SameSource(a, c)>:
103  Holds{property => Equal.trans(Totality.Inspection, Totality.inspect(property, c), Totality.inspect(property, b), Totality.inspect(property, a),
104    bc(property), ab(property))}