proposition: Lemma rclo12_compose clo r: rclo12 (rclo12 clo) r <12= rclo12 clo r.
proof: Proof. intros. induction PR. - apply rclo12_base, IN. - apply rclo12_rclo. eapply rclo12_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco12 pacotac)