law bimp

lawful-words@0.1.0.0 · proof_bytes.bend:46

import Base

46# and(l, and(i, x)) = and(l, x) when l implies i.
47law bimp:
48  for +l: Bool
49  for +i: Bool
50  for +x: Bool
51  for imp: {l == True{} : Bool} -> {i == True{} : Bool}
52  {Bool.and(l, Bool.and(i, x)) == Bool.and(l, x) : Bool}