proposition: Lemma wrespect0_companion clo (RES: wrespectful0 clo): clo <1= cpn0 gf.
proof: Proof. intros. eapply wrespect0_compatible' in RES. eapply (@compatible'0_companion (rclo0 clo)) in RES; [apply RES|]. eapply rclo0_clo_base, PR. Qed.
imports: Program.Basics Paco(paco0 pacotac)