proposition: Lemma grespect5_companion clo (RES: grespectful5 clo): clo <6= cpn5 gf.
proof: Proof. intros. eapply grespect5_compatible' in RES. eapply (@compatible'5_companion (rclo5 (clo \6/ cpn5 gf))); [apply RES|]. apply rclo5_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco5 pacotac)