proposition: Lemma grespect11_companion clo (RES: grespectful11 clo): clo <12= cpn11 gf.
proof: Proof. intros. eapply grespect11_compatible' in RES. eapply (@compatible'11_companion (rclo11 (clo \12/ cpn11 gf))); [apply RES|]. apply rclo11_clo_base. left. apply PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)