proposition: Lemma wrespect1_companion clo (RES: wrespectful1 clo): clo <2= cpn1 gf.
proof: Proof. intros. eapply wrespect1_compatible' in RES. eapply (@compatible'1_companion (rclo1 clo)) in RES; [apply RES|]. eapply rclo1_clo_base, PR. Qed.
imports: Program.Basics Paco(paco1 pacotac)