def same_trans

bendtorch-core@0.1.0.0 · src/autograd/reduce_PROOF.bend:87

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

87def same_trans(-a: Core.Dynamic, -b: Core.Dynamic, -c: Core.Dynamic,
88  -ab: Totality.SameSource(a, b), -bc: Totality.SameSource(b, c)) -> Holds<Totality.SameSource(a, c)>:
89  Holds{property => Equal.trans(Totality.Inspection, Totality.inspect(property, c), Totality.inspect(property, b), Totality.inspect(property, a),
90    bc(property), ab(property))}