proposition: Lemma eqb_equiv : forall b b', b = b' <-> (b = true <-> b' = true).
proof: Proof. intros b b'. split; intro H. subst b'. refl. destruct b. sym. rewrite <- H. refl. destruct b'. rewrite H. refl. refl. Qed.
imports: Coq(ZArith Lia) CoLoR(LogicUtil)