PROOF.cg: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/PROOF.bend as PROOF
Lines 360-367 of bendtorch@1.3.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/PROOF.bend&start_line=360&end_line=367

import Base
import bendtorch@1.3.0.0/main.bend as T

def cg(k: Nat, xs: List<&1, T.FS>, acc: List<&1, T.FS>) -> CGR<k, xs, acc>:
  match k xs:
    case 1n+m Con{x, t}:
      cg_con(m, x, t, acc, cg(m, t, x <> acc))
    case 0n ys:
      cg_base(0n, ys, acc, {==}, go_app(acc, Nil{}, ys))
    case 1n+m Nil{}:
      cg_base(1n+m, Nil{}, acc, {==}, go_app(acc, Nil{}, Nil{}))

Uses (7):
  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@1.3.0.0/PROOF.bend&name=CGR
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cg_base
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=cg_con
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=go_app
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=FS