proposition: Lemma rclo6_compose clo r: rclo6 (rclo6 clo) r <6= rclo6 clo r.
proof: Proof. intros. induction PR. - apply rclo6_base, IN. - apply rclo6_rclo. eapply rclo6_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco6 pacotac)