proposition: Lemma star_stable_inv : forall (A B:Type) (m:M A) (F:A -> M B), stable_inv m -> (forall a:A, stable_inv (F a)) -> stable_inv (star m F).
proof: Proof. unfold stable_inv in |- *; intros. unfold star in |- *; simpl. apply Ole_trans with (m (finv (fun x:A => F x f))); trivial. apply (fmonotonic m); intro x. apply (H0 x f). Qed.
imports: ALEA(Uprop) ALEA(Utheory)