ProofFastW2.nth4_same: law of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w2.bend as ProofFastW2
Lines 149-152 of lawful-bytes@0.1.1.0/proof_fast_w2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&start_line=149&end_line=152

import Base
import lawful-words@0.1.0.0/defs.bend as W

law nth4_same:
  for +j: Nat
  for +c: U32
  {W.nth4(j, c, c, c, c) == c : U32}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=lawful-words@0.1.0.0/defs.bend&name=nth4