proposition: Lemma bool_and_true : forall a b, (bool_and a b = true) = (a = true /\ b = true).
proof: Proof. intros. apply iff_eq; intros. apply conj. induction a; induction b; try discriminate; try assumption. induction a; induction b; try discriminate; try assumption. induction H. rewrite H; rewrite H0; reflexivity. Qed.