ReduceReplayedProof.got: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend as ReduceReplayedProof
Lines 515-523 of bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&start_line=515&end_line=523

import Base
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

def got(+h: List<&2, Api.Effect>, +d: Nat, +f: F32, +i: U32) ->
  {Array.get(F32, Api.arr(h, d, f), i) == (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))) : Array<F32> & F32}:
  Equal.trans(Array<F32> & F32, Array.get(F32, Api.arr(h, d, f), i),
    (Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
    (Api.arr(h, d, f), Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
    eta(Array.get(F32, Api.arr(h, d, f), i)),
    Equal.cong(Array<F32>, Array<F32> & F32, a => (a, Refinement.second(F32, Array.get(F32, Api.arr(h, d, f), i))),
      Refinement.first(F32, Array.get(F32, Api.arr(h, d, f), i)), Api.arr(h, d, f),
      Refinement.law_get_retains(F32, d, Api.arr(h, d, f), i, Api.bal(h, d, f))))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_replayed_proof.bend&name=eta
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=Effect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=arr
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=bal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_get_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second