proposition: Lemma cover_equiv_eq_stable : forall (A:Type)(P Q:set A)(f g:MF A), cover P f -> equiv P Q -> f == g -> cover Q g.
proof: Proof. intros; assert (cover P g). apply cover_eq_stable with f; auto. apply cover_equiv_stable with P; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)