proposition: Lemma grespect9_companion clo (RES: grespectful9 clo): clo <10= cpn9 gf.
proof: Proof. intros. eapply grespect9_compatible' in RES. eapply (@compatible'9_companion (rclo9 (clo \10/ cpn9 gf))); [apply RES|]. apply rclo9_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco9 pacotac)