proposition: Lemma wrespect6_companion clo (RES: wrespectful6 clo): clo <7= cpn6 gf.
proof: Proof. intros. eapply wrespect6_compatible' in RES. eapply (@compatible'6_companion (rclo6 clo)) in RES; [apply RES|]. eapply rclo6_clo_base, PR. Qed.
imports: Program.Basics Paco(paco6 pacotac)