proposition: Lemma rclo9_compose clo r: rclo9 (rclo9 clo) r <9= rclo9 clo r.
proof: Proof. intros. induction PR. - apply rclo9_base, IN. - apply rclo9_rclo. eapply rclo9_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco9 pacotac)