proposition: Lemma grespect6_companion clo (RES: grespectful6 clo): clo <7= cpn6 gf.
proof: Proof. intros. eapply grespect6_compatible' in RES. eapply (@compatible'6_companion (rclo6 (clo \7/ cpn6 gf))); [apply RES|]. apply rclo6_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco6 pacotac)