proposition: Lemma sigma_lub1 : forall (f : natO -m> (natO -O-> U)) n, sigma (lub f) n == lub ((Sigma <_> n) @ f).
proof: Proof. intros; assert (Sigma (lub f) == lub (Sigma @ f)). apply lub_comp_eq with (f:= Sigma); apply sigma_continuous1. apply Oeq_trans with (lub (Sigma @ f) n); auto. Qed.
imports: ALEA(Utheory)