proposition: Lemma eq_dec : forall x y, {E.eq x y}+{~E.eq x y}.
proof: Proof. intros x y. assert (H:=F.eqb_eq x y). destruct (F.eqb x y); [left|right]. - apply -> H; auto. - intro EQ. apply H in EQ. discriminate. Defined.
imports: RelationClasses Bool Morphisms Setoid