law put_bits

lawful-words@0.1.0.0 · proof_bytes.bend:377

import Base

377law put_bits:
378  for +l: Bool
379  for +i: Bool
380  for +x: Bool
381  for +y: Bool
382  for imp1: {l == True{} : Bool} -> {i == True{} : Bool}
383  for imp2: {l == False{} : Bool} -> {y == False{} : Bool}
384  {Bool.and(l, Bool.or(Bool.and(x, Bool.and(i, Bool.not(Bool.and(i, l)))), Bool.and(i, y))) == y : Bool}