F64cmp.andff: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as F64cmp
Lines 273-280 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend&start_line=273&end_line=280

import Base

def andff(+a: Bool, +b: Bool) -> {Bool.and(a, Bool.and(b, False{})) == False{} : Bool}:
  match a b:
    case True{} True{}:
      {==}
    case True{} False{}:
      {==}
    case False{} _:
      {==}

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and