proposition: Lemma cover_compl : forall (A:Type)(P:set A)(f:MF A), cover P f -> cover (compl P) (finv f).
proof: Proof. unfold cover; intros. case (H x); unfold compl,finv; split; intros. apply Ole_trans with ([1-]0); auto. apply Ole_trans with ([1-]1); auto. apply Uinv_le_compat. apply class_double_neg with (P x); auto. Qed.
imports: ALEA(Utheory) ALEA(Sets)