proposition: Lemma grespect3_companion clo (RES: grespectful3 clo): clo <4= cpn3 gf.
proof: Proof. intros. eapply grespect3_compatible' in RES. eapply (@compatible'3_companion (rclo3 (clo \4/ cpn3 gf))); [apply RES|]. apply rclo3_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco3 pacotac)