proposition: Lemma wrespect3_companion clo (RES: wrespectful3 clo): clo <4= cpn3 gf.
proof: Proof. intros. eapply wrespect3_compatible' in RES. eapply (@compatible'3_companion (rclo3 clo)) in RES; [apply RES|]. eapply rclo3_clo_base, PR. Qed.
imports: Program.Basics Paco(paco3 pacotac)