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

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

# depth 0: the two leaves' loops, appended
def b_fm0c(-l: List<&1, T.BG>, -r: List<&1, T.BG>, -n: Nat, +h: Nat, +dm: T.Dm, -l1y: List<&1, T.BG>, +sl: {l1y == l : List<&1, T.BG>}, fl: {T.bleaf_full(l, h, dm, Nil{}) == b_ffmap(h, dm, l) : List<&1, T.DB>}, r1: List<&1, T.BG>, sr: {r1 == r : List<&1, T.BG>}, fr: {T.bleaf_full(r, h, dm, Nil{}) == b_ffmap(h, dm, r) : List<&1, T.DB>}, c: b_MARF<h, dm, l1y, r>) -> b_MRF<0n, T.Halves{l, r}, n, h, dm>:
  match c:
    case b_MARF{l2, s2, fa}:
      b_MRF{List.append(&1, T.BG, l2, r1), app2(T.BG, l2, l, r1, r, Equal.trans(List<&1, T.BG>, l2, l1y, l, s2, sl), sr),
        Equal.trans(List<&1, T.DB>, List.append(&1, T.DB, T.bleaf_full(l, h, dm, Nil{}), T.bleaf_full(r, h, dm, Nil{})), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), b_ffmap(h, dm, List.append(&1, T.BG, l, r)), app2(T.DB, T.bleaf_full(l, h, dm, Nil{}), b_ffmap(h, dm, l), T.bleaf_full(r, h, dm, Nil{}), b_ffmap(h, dm, r), fl, fr),
          Equal.sym(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)),
            Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l, r)), b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => b_ffmap(h, dm, List.append(&1, T.BG, z, r)), l, l1y, Equal.sym(List<&1, T.BG>, l1y, l, sl)),
              Equal.trans(List<&1, T.DB>, b_ffmap(h, dm, List.append(&1, T.BG, l1y, r)), List.append(&1, T.DB, b_ffmap(h, dm, l1y), b_ffmap(h, dm, r)), List.append(&1, T.DB, b_ffmap(h, dm, l), b_ffmap(h, dm, r)), fa, Equal.cong(List<&1, T.BG>, List<&1, T.DB>, z => List.append(&1, T.DB, b_ffmap(h, dm, z), b_ffmap(h, dm, r)), l1y, l, sl)))))}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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=app2
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MARF
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_MRF
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/PROOF.bend&name=b_ffmap
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=BG
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=DB
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Dm
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=Halves
  https://jend.leeeet.dev/definition.txt?path=bendtorch@1.3.0.0/main.bend&name=bleaf_full