proposition: Lemma rclo1_compose clo r: rclo1 (rclo1 clo) r <1= rclo1 clo r.
proof: Proof. intros. induction PR. - apply rclo1_base, IN. - apply rclo1_rclo. eapply rclo1_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco1 pacotac)