proposition: Lemma rclo4_compose clo r: rclo4 (rclo4 clo) r <4= rclo4 clo r.
proof: Proof. intros. induction PR. - apply rclo4_base, IN. - apply rclo4_rclo. eapply rclo4_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco4 pacotac)