proposition: Lemma rclo3_compose clo r: rclo3 (rclo3 clo) r <3= rclo3 clo r.
proof: Proof. intros. induction PR. - apply rclo3_base, IN. - apply rclo3_rclo. eapply rclo3_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco3 pacotac)