ProofFastW2.or_false: def of lawful-bytes@0.1.1.0
Import: import lawful-bytes@0.1.1.0/proof_fast_w2.bend as ProofFastW2
Lines 105-110 of lawful-bytes@0.1.1.0/proof_fast_w2.bend: https://jend.leeeet.dev/read.txt?path=lawful-bytes@0.1.1.0/proof_fast_w2.bend&start_line=105&end_line=110

import Base

def or_false(-p: Nat, +b: Bool, +t: Word(p)) -> {WCon{Bool.or(b, False{}), t} == WCon{b, t} : Word(1n+p)}:
  match b:
    case False{}:
      {==}
    case True{}:
      {==}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con