LAWS.permute_rank: law of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/LAWS.bend as LAWS
Lines 309-313 of bendtorch@1.3.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/LAWS.bend&start_line=309&end_line=313

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

# LAW (permute_rank): permuting by p gives as many axes as p has, so a permutation of the axes keeps the rank.
law permute_rank:
  for +s: List<&2, Nat>
  for p: List<&2, Nat>
  {TT.rank(TT.permuted(s, p)) == List.length(&2, Nat, p) : Nat}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=permuted
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/tensor.bend&name=rank