proposition: Lemma wrespect10_companion clo (RES: wrespectful10 clo): clo <11= cpn10 gf.
proof: Proof. intros. eapply wrespect10_compatible' in RES. eapply (@compatible'10_companion (rclo10 clo)) in RES; [apply RES|]. eapply rclo10_clo_base, PR. Qed.
imports: Program.Basics Paco(paco10 pacotac)