law eq_true_of_and_left

bend-mathlib@0.8.1.0 · bool.bend:448

import Base

448# If a and b is true then a is true.
449law eq_true_of_and_left:
450  for a: Bool
451  for -b: Bool
452  for h: {Bool.and(a, b) == True{} : Bool}
453  {a == True{} : Bool}