proposition: Lemma wcompat3_compat clo (WCMP: wcompatible3 clo) : compatible3 (gupaco3 gf clo).
proof: Proof. econstructor. { red; intros. eapply gpaco3_mon. apply IN. apply LE. apply LE. } intros. apply gpaco3_unfold in PR; [|apply gf_mon]. induction PR. - destruct IN; cycle 1. + eapply gf_mon. apply H. intros. apply gpaco3_base, PR. + eapply gf_mon. apply H. intros. apply gpaco3_gupaco. apply gf_mon. eapply gupaco3_mon. apply PR. intros. apply gpaco3_step. apply gf_mon. eapply gf_mon. destruct PR0 as [X|X]; apply X. intros. apply gpaco3_base, PR1. - eapply gf_mon, gpaco3_gupaco, gf_mon. apply WCMP. eapply WCMP. apply IN. intros. apply H, PR. Qed.
imports: Program.Basics Paco(paco3 pacotac)