proposition: Lemma rclo6_compat clo (COM: compatible6 clo): compatible6 (rclo6 clo).
proof: Proof. econstructor. - apply rclo6_mon. - intros. induction PR. + eapply gf_mon. apply IN. intros. eapply rclo6_base. apply PR. + eapply gf_mon. * eapply COM. eapply COM. apply IN. apply H. * intros. eapply rclo6_clo. apply PR. Qed.
imports: Program.Basics Paco(paco6 pacotac)