[STATEMENT]
lemma of_int_or_eq:
  \<open>of_int (k OR l) = of_int k OR of_int l\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. of_int (k OR l) = of_int k OR of_int l
[PROOF STEP]
by (rule bit_eqI) (simp add: bit_of_int_iff bit_or_iff Bit_Operations.bit_or_iff)