proposition: Lemma cover_mult_fun : forall (A:Type)(P:set A)(cP : MF A)(f g:A->U), (forall x, P x -> f x == g x) -> cover P cP -> forall x, cP x * f x == cP x * g x.
proof: Proof. intros. apply (cover_elim H0 x); auto; intuition. rewrite H3; repeat Usimpl; auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)