proposition: Lemma wrespect2_companion clo (RES: wrespectful2 clo): clo <3= cpn2 gf.
proof: Proof. intros. eapply wrespect2_compatible' in RES. eapply (@compatible'2_companion (rclo2 clo)) in RES; [apply RES|]. eapply rclo2_clo_base, PR. Qed.
imports: Program.Basics Paco(paco2 pacotac)