proposition: Lemma grespect12_companion clo (RES: grespectful12 clo): clo <13= cpn12 gf.
proof: Proof. intros. eapply grespect12_compatible' in RES. eapply (@compatible'12_companion (rclo12 (clo \13/ cpn12 gf))); [apply RES|]. apply rclo12_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco12 pacotac)