proposition: Lemma eqb_eq : forall x y, eqb x y = true <-> E.eq x y.
proof: Proof. intros x y. unfold eqb. destruct F.eq_dec as [EQ|NEQ]. - auto with *. - split. + discriminate. + intro EQ; elim NEQ; auto. Qed.
imports: RelationClasses Bool Morphisms Setoid