proposition: Lemma grespect13_companion clo (RES: grespectful13 clo): clo <14= cpn13 gf.
proof: Proof. intros. eapply grespect13_compatible' in RES. eapply (@compatible'13_companion (rclo13 (clo \14/ cpn13 gf))); [apply RES|]. apply rclo13_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco13 pacotac)