#ifndef VERIFAST_BITOPS_EXTENDED_H
#define VERIFAST_BITOPS_EXTENDED_H

/*@
// TODO: Can we remove this?
lemma void bitand_idempotent_right(int l, int r);
requires true;
ensures (l & r) == ((l & r) & r);
@*/

#endif /* VERIFAST_BITOPS_EXTENDED_H */