proposition: Lemma rclo2_compose clo r: rclo2 (rclo2 clo) r <2= rclo2 clo r.
proof: Proof. intros. induction PR. - apply rclo2_base, IN. - apply rclo2_rclo. eapply rclo2_mon; [apply IN|apply H]. Qed.
imports: Program.Basics Paco(paco2 pacotac)