proposition: Lemma grespect7_compatible' clo (RES: grespectful7 clo): compatible'7 (rclo7 (clo \8/ cpn7 gf)).
proof: Proof. apply wrespect7_compatible'. econstructor. { red; intros. destruct IN. - left. eapply RES; [apply H|]. apply LE. - right. eapply cpn7_mon; [apply H|]. apply LE. } intros. destruct PR. - eapply RES.(grespect7_respect) in H; [|apply LE|apply GF]. apply (@compat7_compat gf (rclo7 (cpn7 gf))) in H. 2: { apply rclo7_compat; [apply gf_mon|]. apply cpn7_compat. apply gf_mon. } eapply gf_mon; [apply H|]. intros. apply rclo7_clo. right. exists (rclo7 (cpn7 gf)). { apply rclo7_compat; [apply gf_mon|]. apply cpn7_compat. apply gf_mon. } eapply rclo7_mon; [eapply PR|]. intros. eapply rclo7_mon_gen; [eapply PR0|..]. + intros. destruct PR1. * left. apply H0. * right. apply cpn7_gupaco; [apply gf_mon|apply H0]. + intros. apply PR1. - eapply gf_mon. + apply (@compat7_compat gf (rclo7 (cpn7 gf))). { apply rclo7_compat; [apply gf_mon|]. apply cpn7_compat. apply gf_mon. } eapply rclo7_clo_base. eapply cpn7_mon; [apply H|apply GF]. + intros. eapply rclo7_mon_gen; [eapply PR|..]. * intros. right. apply PR0. * intros. apply PR0. Qed.
imports: Program.Basics Paco(paco7 pacotac)