Transcong.cite: def of bolt@1.27.0.0
Import: import bolt@1.27.0.0/src/rules/style/transcong.bend as Transcong
Lines 119-122 of bolt@1.27.0.0/src/rules/style/transcong.bend: https://jend.leeeet.dev/read.txt?path=bolt@1.27.0.0/src/rules/style/transcong.bend&start_line=119&end_line=122

import Base
import bolt@1.27.0.0/src/finding.bend as F

# the finding at the `Equal.trans` leaf
def cite(+ll: U32, +cc: U32, +path: String) -> F.Finding:
  F.Finding{path, ll, cc, 11, "transcong",
    "this Equal.trans is fed an Equal.cong: rewrite instead, `%e : {F(_) == c : T}` with the other proof below it, which names the motive once and drops the middle term."}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bolt@1.27.0.0/src/finding.bend&name=Finding