proposition: Lemma okup_eq_compat : forall (A:Type) (p p':U) (e e':Distr A) (q q':A-o>U), p == p' -> q == q' -> e == e' -> okup p e q -> okup p' e' q'.
proof: Proof. unfold okup; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. apply Ole_trans with (mu e' q); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)