law true_and

bend-mathlib@0.8.1.0 · bool.bend:90

import Base

90# True is a left identity for and: true and a is a.
91law true_and:
92  for -a: Bool
93  {Bool.and(True{}, a) == a : Bool}