proposition: Lemma wrespect9_companion clo (RES: wrespectful9 clo): clo <10= cpn9 gf.
proof: Proof. intros. eapply wrespect9_compatible' in RES. eapply (@compatible'9_companion (rclo9 clo)) in RES; [apply RES|]. eapply rclo9_clo_base, PR. Qed.
imports: Program.Basics Paco(paco9 pacotac)