proposition: Lemma grespect10_companion clo (RES: grespectful10 clo): clo <11= cpn10 gf.
proof: Proof. intros. eapply grespect10_compatible' in RES. eapply (@compatible'10_companion (rclo10 (clo \11/ cpn10 gf))); [apply RES|]. apply rclo10_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco10 pacotac)