proposition: Lemma rclo0_compose clo r: rclo0 (rclo0 clo) r <0= rclo0 clo r.
proof: Proof. intros. induction PR. - apply rclo0_base, IN. - apply rclo0_rclo. eapply rclo0_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco0 pacotac)