proposition: Lemma rclo13_compose clo r: rclo13 (rclo13 clo) r <13= rclo13 clo r.
proof: Proof. intros. induction PR. - apply rclo13_base, IN. - apply rclo13_rclo. eapply rclo13_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco13 pacotac)