proposition: Lemma wrespect8_companion clo (RES: wrespectful8 clo): clo <9= cpn8 gf.
proof: Proof. intros. eapply wrespect8_compatible' in RES. eapply (@compatible'8_companion (rclo8 clo)) in RES; [apply RES|]. eapply rclo8_clo_base, PR. Qed.
imports: Program.Basics Paco(paco8 pacotac)