law and_eq_true

bend-mathlib@0.8.1.0 · bool.bend:476

import Base

476# If a and b are both true then a and b is true.
477law and_eq_true:
478  for a: Bool
479  for -b: Bool
480  for ha: {a == True{} : Bool}
481  for hb: {b == True{} : Bool}
482  {Bool.and(a, b) == True{} : Bool}