proposition: Lemma grespect7_companion clo (RES: grespectful7 clo): clo <8= cpn7 gf.
proof: Proof. intros. eapply grespect7_compatible' in RES. eapply (@compatible'7_companion (rclo7 (clo \8/ cpn7 gf))); [apply RES|]. apply rclo7_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco7 pacotac)