proposition: Lemma grespect8_companion clo (RES: grespectful8 clo): clo <9= cpn8 gf.
proof: Proof. intros. eapply grespect8_compatible' in RES. eapply (@compatible'8_companion (rclo8 (clo \9/ cpn8 gf))); [apply RES|]. apply rclo8_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco8 pacotac)