proposition: Lemma grespect14_companion clo (RES: grespectful14 clo): clo <15= cpn14 gf.
proof: Proof. intros. eapply grespect14_compatible' in RES. eapply (@compatible'14_companion (rclo14 (clo \15/ cpn14 gf))); [apply RES|]. apply rclo14_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco14 pacotac)