proposition: Lemma compatible'10_companion clo (RES: compatible'10 clo): clo <11= cpn10 gf.
proof: Proof. assert (MON: monotone10 gf'10). { econstructor. apply LE, IN. eapply gf_mon, LE. apply IN. } assert (CPN: clo <11= cpn10 gf'10). { intros. econstructor. apply RES. apply PR. } intros. apply CPN in PR. econstructor; [|apply PR]. econstructor; [apply cpn10_mon|]; intros. assert (PR1: cpn10 gf'10 (gf r) <10= cpn10 gf'10 (gf'10 (cpn10 gf r))). { intros. eapply cpn10_mon. apply PR1. intros. assert (TMP: gf (cpn10 gf r) <10= (cpn10 gf r /10\ gf (cpn10 gf r))). { split; [apply cpn10_step; [apply gf_mon|]|]; assumption. } apply TMP. eapply gf_mon. apply PR2. intros. apply cpn10_base; assumption. } apply PR1 in PR0. clear PR1. eapply compat10_compat with (gf:=gf'10) in PR0; [|apply cpn10_compat, MON]. eapply gf_mon; [apply PR0|]. intros. eapply cpn10_cpn; [apply MON|]. eapply cpn10_mon; [apply PR1|]. intros. econstructor; [|apply PR2]. apply compat10_compatible', cpn10_compat, gf_mon. Qed.
imports: Program.Basics Paco(paco10 pacotac)