proposition: Lemma rclo14_compose clo r: rclo14 (rclo14 clo) r <14= rclo14 clo r.
proof: Proof. intros. induction PR. - apply rclo14_base, IN. - apply rclo14_rclo. eapply rclo14_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco14 pacotac)