proposition: Lemma wrespect11_companion clo (RES: wrespectful11 clo): clo <12= cpn11 gf.
proof: Proof. intros. eapply wrespect11_compatible' in RES. eapply (@compatible'11_companion (rclo11 clo)) in RES; [apply RES|]. eapply rclo11_clo_base, PR. Qed.
imports: Program.Basics Paco(paco11 pacotac)