proposition: Lemma compatible'3_companion clo (RES: compatible'3 clo): clo <4= cpn3 gf.
proof: Proof. assert (MON: monotone3 gf'3). { econstructor. apply LE, IN. eapply gf_mon, LE. apply IN. } assert (CPN: clo <4= cpn3 gf'3). { intros. econstructor. apply RES. apply PR. } intros. apply CPN in PR. econstructor; [|apply PR]. econstructor; [apply cpn3_mon|]; intros. assert (PR1: cpn3 gf'3 (gf r) <3= cpn3 gf'3 (gf'3 (cpn3 gf r))). { intros. eapply cpn3_mon. apply PR1. intros. assert (TMP: gf (cpn3 gf r) <3= (cpn3 gf r /3\ gf (cpn3 gf r))). { split; [apply cpn3_step; [apply gf_mon|]|]; assumption. } apply TMP. eapply gf_mon. apply PR2. intros. apply cpn3_base; assumption. } apply PR1 in PR0. clear PR1. eapply compat3_compat with (gf:=gf'3) in PR0; [|apply cpn3_compat, MON]. eapply gf_mon; [apply PR0|]. intros. eapply cpn3_cpn; [apply MON|]. eapply cpn3_mon; [apply PR1|]. intros. econstructor; [|apply PR2]. apply compat3_compatible', cpn3_compat, gf_mon. Qed.
imports: Program.Basics Paco(paco3 pacotac)