proposition: Lemma orP : forall (b1 b2: bool), reflect (b1 \/ b2) (b1 || b2).
proof: Proof. intros; apply iff_reflect; split; case_eq b1; case_eq b2; intros; try easy; try compute in *. destruct H1 as [H1a | H1b ]; easy. left. easy. left. easy. right. easy. Qed.
imports: Bool ZArith BVList Logic