proposition: Lemma grespect0_companion clo (RES: grespectful0 clo): clo <1= cpn0 gf.
proof: Proof. intros. eapply grespect0_compatible' in RES. eapply (@compatible'0_companion (rclo0 (clo \1/ cpn0 gf))); [apply RES|]. apply rclo0_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco0 pacotac)