proposition: Lemma wrespect2_compatible' clo (RES: wrespectful2 clo): compatible'2 (rclo2 clo).
proof: Proof. intros. econstructor. apply rclo2_mon. intros. destruct RES. split. { eapply rclo2_mon. apply PR. intros. apply PR0. } induction PR; intros. - eapply gf_mon. apply IN. intros. apply rclo2_base, PR. - eapply gf_mon. + eapply wrespect2_respect0; [|apply H|apply IN]. intros. eapply rclo2_mon; intros; [apply LE, PR|apply PR0]. + intros. apply rclo2_rclo, PR. Qed.
imports: Program.Basics Paco(paco2 pacotac)