proposition: Lemma paco_mon_gen T0 gf gf' r r' x (PR: @paco T0 gf r x) (LEgf: gf <2= gf') (LEr: r <1= r'): paco gf' r' x.
proof: Proof. revert x PR. cofix CIH. intros. apply paco_observe in PR. destruct PR as []. do 2 econstructor. - intros. specialize (LE x0 PR). destruct LE. + left. apply CIH, H. + right. apply LEr, H. - apply LEgf, SIM. Qed.
imports: Paco(pacotac_internal paconotation_internal)