proposition: Lemma implyP2 : forall (b1 b2 b3: bool), reflect (b1 -> b2 -> b3) (b1 --> b2 --> b3).
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