proposition: Lemma hahn__eqb_split : forall b1 b2 : bool, (b1 -> b2) -> (b2 -> b1) -> b1 = b2.
proof: Proof. intros [] [] H H'; unfold is_true in *; auto using sym_eq. Qed.
imports: Bool Arith ZArith String ClassicalDescription FunctionalExtensionality