proposition: Lemma cover_eq_stable : forall (A:Type)(P:set A)(f g:MF A), cover P f -> f == g -> cover P g.
proof: Proof. unfold cover; intros. case (H x); case (ford_eq_elim H0 x); split; intros; apply Ole_trans with (f x); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)