AxisPROOF.inverse_involution: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/axis_PROOF.bend as AxisPROOF
Lines 14-17 of bendtorch-core@0.1.0.0/src/tensor/axis_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_PROOF.bend&start_line=14&end_line=17

import Base
import bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend as Axis
import bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend as Algebra

def inverse_involution(-rank: Nat, -axes: List<&2, Nat>, certificate: Algebra.Facts<rank, axes>) ->
  {Axis.inverse_axes(rank, Axis.inverse_axes(rank, axes)) == axes : List<&2, Nat>}:
  Algebra.Certified{iv, selected, restored, lists, product, fit} = certificate
  restored

Uses (4):
  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=bendtorch-core@0.1.0.0/src/tensor/axis_algebra.bend&name=Facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/axis_spec.bend&name=inverse_axes