proposition: Lemma compat1_wcompat clo (CMP: compatible1 clo): wcompatible1 clo.
proof: Proof. econstructor. apply CMP. intros. apply CMP in PR. eapply gf_mon. apply PR. intros. apply gpaco1_clo, PR0. Qed.
imports: Program.Basics Paco(paco1 pacotac)