proposition: Lemma wrespect7_companion clo (RES: wrespectful7 clo): clo <8= cpn7 gf.
proof: Proof. intros. eapply wrespect7_compatible' in RES. eapply (@compatible'7_companion (rclo7 clo)) in RES; [apply RES|]. eapply rclo7_clo_base, PR. Qed.
imports: Program.Basics Paco(paco7 pacotac)