proposition: Lemma implyP : 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 *; now apply H1. Qed.
imports: Bool ZArith BVList Logic