proposition: Lemma rclo12_wcompat clo (COM: wcompatible12 clo): wcompatible12 (rclo12 clo).
proof: Proof. econstructor. - apply rclo12_mon. - intros. induction PR. + eapply gf_mon. apply IN. intros. apply gpaco12_base. apply PR. + eapply gf_mon. * eapply COM. eapply COM. apply IN. apply H. * intros. eapply gpaco12_gupaco. apply gf_mon. eapply gupaco12_mon_gen; intros; [apply PR|apply gf_mon|apply PR0| |apply PR0]. apply rclo12_clo_base, PR0. Qed.
imports: Program.Basics Paco(paco12 pacotac)