proposition: Lemma cover_incl_eq: forall (A:Type)(P:set A)(f g:MF A), cover P f -> cover P g -> f == g.
proof: Proof. intros; apply Ole_antisym. apply (cover_incl_fle H H0); auto. apply (cover_incl_fle H0 H); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)