proposition: Lemma grespect2_companion clo (RES: grespectful2 clo): clo <3= cpn2 gf.
proof: Proof. intros. eapply grespect2_compatible' in RES. eapply (@compatible'2_companion (rclo2 (clo \3/ cpn2 gf))); [apply RES|]. apply rclo2_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco2 pacotac)