proposition: Lemma grespect1_companion clo (RES: grespectful1 clo): clo <2= cpn1 gf.
proof: Proof. intros. eapply grespect1_compatible' in RES. eapply (@compatible'1_companion (rclo1 (clo \2/ cpn1 gf))); [apply RES|]. apply rclo1_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco1 pacotac)