ProofList.decb_if: def of lawful-fields@0.1.1.0
Import: import lawful-fields@0.1.1.0/proof_list.bend as ProofList
Lines 443-450 of lawful-fields@0.1.1.0/proof_list.bend: https://jend.leeeet.dev/read.txt?path=lawful-fields@0.1.1.0/proof_list.bend&start_line=443&end_line=450

import Base
import lawful-fields@0.1.1.0/defs.bend as F
import lawful-arrays@0.1.0.0/proof_base.bend as AB

# 2^32 must never take part in a conversion (the checker would expand it), so
# the bound stays a variable M and the law instantiates it.
def decb_if(+n: Nat, b: Bool, hb: {b == True{} : Bool}) -> {F.decb.if(n, b) == Some{n} : Maybe<&2, Nat>}:
  match b:
    case True{}:
      {==}
    case False{}:
      Empty.absurd({F.decb.if(n, False{}) == Some{n} : Maybe<&2, Nat>}, AB.false_ne_true(hb))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=lawful-arrays@0.1.0.0/proof_base.bend&name=false_ne_true
  https://jend.leeeet.dev/definition.txt?path=lawful-fields@0.1.1.0/defs.bend&name=decb.if