PROOF.cmp.split: def of bend-kit-collections@0.1.4.1
Import: import bend-kit-collections@0.1.4.1/PROOF.bend as PROOF
Lines 501-515 of bend-kit-collections@0.1.4.1/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-kit-collections@0.1.4.1/PROOF.bend&start_line=501&end_line=515

import Base
import bend-kit-collections@0.1.4.1/omap.bend as O

# Proves a goal about O.Cmp.case by one case per comparison result.
def cmp.split(
  -A: Type, -B: Type, -F: A -> B, -G: B, c: Cmp, -f1: Unit -> A,
  -f2: Unit -> A, -f3: Unit -> A,
  hl: {c == LT{} : Cmp} -> {F(f1(Unit{})) == G : B},
  he: {c == EQ{} : Cmp} -> {F(f2(Unit{})) == G : B},
  hg: {c == GT{} : Cmp} -> {F(f3(Unit{})) == G : B}
) -> {F(O.Cmp.case(A, c, f1, f2, f3)) == G : B}:
  match c:
    case LT{}:
      hl({==})
    case EQ{}:
      he({==})
    case GT{}:
      hg({==})

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bend-kit-collections@0.1.4.1/omap.bend&name=Cmp.case