coq.file += "Coq/BitLemmas.v";

library b4fc_bit : cbits;

logic boolean LogicalBitTest(integer, integer) := \bit_test;

predicate BitTest (integer, integer) := \bit_test;