proposition: Lemma wrespect4_companion clo (RES: wrespectful4 clo): clo <5= cpn4 gf.
proof: Proof. intros. eapply wrespect4_compatible' in RES. eapply (@compatible'4_companion (rclo4 clo)) in RES; [apply RES|]. eapply rclo4_clo_base, PR. Qed.
imports: Program.Basics Paco(paco4 pacotac)