law eq_true_of_and_right

bend-mathlib@0.8.1.0 · bool.bend:462

import Base

462# If a and b is true then b is true.
463law eq_true_of_and_right:
464  for a: Bool
465  for -b: Bool
466  for h: {Bool.and(a, b) == True{} : Bool}
467  {b == True{} : Bool}