proposition: Lemma grespect4_companion clo (RES: grespectful4 clo): clo <5= cpn4 gf.
proof: Proof. intros. eapply grespect4_compatible' in RES. eapply (@compatible'4_companion (rclo4 (clo \5/ cpn4 gf))); [apply RES|]. apply rclo4_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco4 pacotac)